From b9f36ae0027e52da925416630ccad5d4b84779e9 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 6 Jul 2010 04:00:42 +0000
Subject: Fixes for doubled-statistics (bug 171), a fix to muzzled builds and
 some minor code cleanup found while searching for additional cases.  Closes
 bug 171.

---
 src/util/output.cpp | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/util/output.cpp')

diff --git a/src/util/output.cpp b/src/util/output.cpp
index 8a0bdd298..36ab77dd0 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -142,7 +142,6 @@ void TraceC::printf(string tag, const char* fmt, ...) {
 
 NullDebugC Debug CVC4_PUBLIC;
 NullC Warning CVC4_PUBLIC;
-NullC Warning CVC4_PUBLIC;
 NullC Message CVC4_PUBLIC;
 NullC Notice CVC4_PUBLIC;
 NullC Chat CVC4_PUBLIC;
-- 
cgit v1.2.3