diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/util/output.h | 7 |
1 files changed, 6 insertions, 1 deletions
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 { |