summaryrefslogtreecommitdiff
path: root/src/main/driver_unified.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r--src/main/driver_unified.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 2a9202898..cad662d90 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -26,6 +26,7 @@
// This must come before PORTFOLIO_BUILD.
#include "cvc4autoconfig.h"
+#include "base/tls.h"
#include "base/configuration.h"
#include "base/output.h"
#include "expr/expr_iomanip.h"
@@ -55,7 +56,7 @@ using namespace CVC4::main;
namespace CVC4 {
namespace main {
/** Global options variable */
- CVC4_THREADLOCAL(Options*) pOptions;
+ CVC4_THREAD_LOCAL Options* pOptions;
/** Full argv[0] */
const char *progPath;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback