summaryrefslogtreecommitdiff
path: root/src/util/output.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/output.cpp')
-rw-r--r--src/util/output.cpp3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 88628481f..29de4c360 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -31,6 +31,9 @@ ostream null_os(&null_sb);
NullC nullCvc4Stream CVC4_PUBLIC;
+const std::string CVC4ostream::s_tab = " ";
+const int CVC4ostream::s_indentIosIndex = ios_base::xalloc();
+
DebugC DebugChannel CVC4_PUBLIC (&cout);
WarningC WarningChannel CVC4_PUBLIC (&cerr);
MessageC MessageChannel CVC4_PUBLIC (&cout);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback