diff options
Diffstat (limited to 'src/util/statistics.cpp')
-rw-r--r-- | src/util/statistics.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index a6b20934c..e5bb6e532 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -113,7 +113,6 @@ void StatisticsBase::flushInformation(std::ostream &out) const { } s->flushStat(out); } - out << std::endl; #endif /* CVC4_STATISTICS_ON */ } @@ -126,8 +125,8 @@ void StatisticsBase::safeFlushInformation(int fd) const { safe_print(fd, s_regDelim); } s->safeFlushStat(fd); + safe_print(fd, "\n"); } - safe_print(fd, "\n"); #endif /* CVC4_STATISTICS_ON */ } |