From 013daeafb5bca803592ffa8120d360ecc58dfd2d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Mar 2016 12:35:07 +0100
Subject: [PATCH] better position for the legend
---
benchmark/visualize.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/benchmark/visualize.py b/benchmark/visualize.py
index 2b017ee92..3456b4b4b 100755
--- a/benchmark/visualize.py
+++ b/benchmark/visualize.py
@@ -29,7 +29,7 @@ results = list(results)
timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
for timing in timings:
plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
-plt.legend(timings, loc='lower left')
+plt.legend(timings, loc='upper left')
plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
plt.subplots_adjust(bottom=0.2) # more space for the commit labels
--
GitLab