From b249f10578a078e032ed21bc7a3812b70d200c4d Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 3 Aug 2018 05:59:23 -0700 Subject: [PATCH] Fix printing statistics in case of signals. (#2267) --- src/util/statistics.cpp | 3 +-- 1 file changed, 1 insertion(+), 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 */ } -- 2.30.2