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