Print a newline at the end of timing tables

This, for example, improves the CI display, so that `$ echo
'end:coq.test'` does not appear on the same line as the end of the
timing table.

1 files changed, 1 insertions, 0 deletions

diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py
index c4620f5b50..a3078af4a1 100644
--- a/tools/TimeFileMaker.py
+++ b/tools/TimeFileMaker.py
@@ -468,6 +468,7 @@ def make_table_string(stats_dict,
                       for name in names])
 
 def print_or_write_table(table, files):
+    if table[-1] != '\n': table += '\n'
     if len(files) == 0 or '-' in files:
         if hasattr(sys.stdout, 'buffer'):
             sys.stdout.buffer.write(table.encode("utf-8"))