diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/util/output.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/util/output.h b/src/util/output.h index dd5007747..9efb4110e 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -169,10 +169,11 @@ public: CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { if(d_os != NULL) { d_os = &(*d_os << pf); - } - if (pf == d_endl) { - for (unsigned i = 0; i < d_indent; ++ i) { - d_os = &(*d_os << '\t'); + + if (pf == d_endl) { + for (unsigned i = 0; i < d_indent; ++ i) { + d_os = &(*d_os << '\t'); + } } } return *this; |