summaryrefslogtreecommitdiff
path: root/src/util/statistics.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/statistics.cpp')
-rw-r--r--src/util/statistics.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 9273f2167..04078ef50 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -112,8 +112,8 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
out << d_prefix << s_regDelim;
}
s->flushStat(out);
- out << std::endl;
}
+ out << std::endl;
#endif /* CVC4_STATISTICS_ON */
}
@@ -126,8 +126,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 */
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback