diff options
Diffstat (limited to 'src/main/main.h')
| -rw-r--r-- | src/main/main.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/main/main.h b/src/main/main.h index d56684d7d..350578ffa 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -52,6 +52,12 @@ extern const char *progName; */ extern bool segvNoSpin; +/** + * Keep a copy of the options around globally, so that signal handlers can + * access it. + */ +extern struct Options options; + /** Parse argc/argv and put the result into a CVC4::Options struct. */ int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); |