diff options
author | Will Dietz <w@wdtz.org> | 2017-11-07T20·42-0600 |
---|---|---|
committer | Will Dietz <w@wdtz.org> | 2017-11-14T18·39-0600 |
commit | 9d7ce0bf45fe4b77f5483929609faad25a66ab8e (patch) | |
tree | 624e5257a7b7a75328f37d59071228f78c070b21 /src/libmain/shared.hh | |
parent | 2f5789c5d6e779ae246659b2974560f14e24ac31 (diff) |
anchor nix::Exit exception
Diffstat (limited to 'src/libmain/shared.hh')
-rw-r--r-- | src/libmain/shared.hh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/libmain/shared.hh b/src/libmain/shared.hh index 9219dbed8325..1dcc4f0ac942 100644 --- a/src/libmain/shared.hh +++ b/src/libmain/shared.hh @@ -17,6 +17,7 @@ public: int status; Exit() : status(0) { } Exit(int status) : status(status) { } + virtual ~Exit(); }; int handleExceptions(const string & programName, std::function<void()> fun); |