diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-12 20:26:56 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-12 20:26:56 +0000 |
| commit | 42bd7611c9a09b4458fbc1076606850628880f3a (patch) | |
| tree | ab3b5f2fc40affeae20beaab447dced52f993d3a /src/util/output.h | |
| parent | 8316697801a73a14a2fe3845e0d0f5add63a18be (diff) | |
Fix to compile out Debug(...) << ... statements in optimized mode. Someone please look to see if it makes sense.
Diffstat (limited to 'src/util/output.h')
| -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 { |