From adf6398383d94fa4f68ef9ba50c29ea9b6ac68e1 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Fri, 12 Feb 2010 20:30:24 +0000
Subject: build fix

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

(limited to 'src/util')

diff --git a/src/util/output.cpp b/src/util/output.cpp
index 01a485136..fdc54d9b5 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -25,7 +25,7 @@ namespace CVC4 {
 null_streambuf null_sb;
 std::ostream null_os(&null_sb);
 
-DebugC   Debug  (&std::cout);
+DebugC   DebugOut  (&std::cout);
 WarningC Warning(&std::cerr);
 MessageC Message(&std::cout);
 NoticeC  Notice (&std::cout);
-- 
cgit v1.2.3