diff options
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/main.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/main/main.h b/src/main/main.h index 7e0bf6b65..b2e6e401b 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -47,6 +47,7 @@ extern CVC4::StatisticsRegistry* pStatistics; */ extern bool segvNoSpin; +/** The options currently in play */ extern Options options; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ |