From 4b77018c85eb58d4b838ee04b9b453add24f9397 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Mar 2018 16:49:14 +0100
Subject: [PATCH] fix benchmark export

---
 benchmark/export.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchmark/export.py b/benchmark/export.py
index fd6e21f84..c3269c242 100755
--- a/benchmark/export.py
+++ b/benchmark/export.py
@@ -40,7 +40,7 @@ if args.commits:
 results = list(results)
 
 for datapoint in results:
-    times = ''.join(datapoint.times)
+    times = '\n'.join(datapoint.times)
     commit = datapoint.commit
     print("Sending {}...".format(commit), end='')
     date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8')
-- 
GitLab