From 42bd7611c9a09b4458fbc1076606850628880f3a Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Fri, 12 Feb 2010 20:26:56 +0000
Subject: [PATCH] Fix to compile out Debug(...) << ... statements in optimized
 mode. Someone please look to see if it makes sense.

---
 src/util/output.h | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/util/output.h b/src/util/output.h
index 8ba1ea26b..f897fd1ca 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -90,7 +90,12 @@ public:
 };/* class Debug */
 
 /** The debug output singleton */
-extern DebugC Debug CVC4_PUBLIC;
+extern DebugC DebugOut CVC4_PUBLIC;
+#ifdef CVC4_DEBUG
+  #define Debug DebugOut
+#else
+  #define Debug if(0) DebugOut
+#endif
 
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
-- 
2.30.2