summaryrefslogtreecommitdiff
path: root/src/main/main.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/main.h')
-rw-r--r--src/main/main.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/main/main.h b/src/main/main.h
index dcb5c2a0a..8a5d0971e 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -17,8 +17,8 @@
#include <exception>
#include <string>
-#include "base/exception.h"
#include "base/tls.h"
+#include "base/exception.h"
#include "cvc4autoconfig.h"
#include "expr/expr_manager.h"
#include "options/options.h"
@@ -54,7 +54,7 @@ extern CVC4::TimerStat* pTotalTime;
extern bool segvSpin;
/** A pointer to the options in play */
-extern CVC4_THREADLOCAL(Options*) pOptions;
+extern CVC4_THREAD_LOCAL Options* pOptions;
/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */
void cvc4_init() throw(Exception);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback