From 5e619ab6d4622403cc427c17f4282900deb940d5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 13 Sep 2010 22:13:36 +0000
Subject: statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats
 is given

---
 src/main/main.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/main/main.cpp')

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 0b962bc9b..235ebb354 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -43,7 +43,12 @@ using namespace CVC4::parser;
 using namespace CVC4::main;
 
 static Result lastResult;
-static struct Options options;
+
+namespace CVC4 {
+  namespace main {
+    struct Options options;
+  }/* CVC4::main namespace */
+}/* CVC4 namespace */
 
 int runCvc4(int argc, char* argv[]);
 void doCommand(SmtEngine&, Command*);
-- 
cgit v1.2.3