diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
| commit | 6a4af721d1dc55f1dc6454014c08f87465398a54 (patch) | |
| tree | 178f006869c0c4af6b6c71f46b55c28de643c7bd /src/util/output.cpp | |
| parent | 1ce0650dcf8ce30424b546deb540974cc510c215 (diff) | |
--disable-tracing at configure time now disables Trace() and Debug() gestures both.
Diffstat (limited to 'src/util/output.cpp')
| -rw-r--r-- | src/util/output.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/output.cpp b/src/util/output.cpp index 48a7d51fd..5acee360f 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -45,7 +45,7 @@ DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout); #ifndef CVC4_MUZZLE -# ifdef CVC4_DEBUG +# if defined(CVC4_DEBUG) && defined(CVC4_TRACING) int DebugC::printf(const char* tag, const char* fmt, ...) { if(d_tags.find(string(tag)) == d_tags.end()) { @@ -77,7 +77,7 @@ int DebugC::printf(std::string tag, const char* fmt, ...) { return retval; } -# endif /* CVC4_DEBUG */ +# endif /* CVC4_DEBUG && CVC4_TRACING */ int WarningC::printf(const char* fmt, ...) { // chop off output after 1024 bytes |