From 658c756f4bc79c6998ba6be65fcddf7c771590af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 24 Mar 2018 16:11:07 +0100
Subject: [PATCH] gitlab-extract: show which commit the bad line was in

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

diff --git a/benchmark/parse_log.py b/benchmark/parse_log.py
index 29ce97312..310c7822d 100644
--- a/benchmark/parse_log.py
+++ b/benchmark/parse_log.py
@@ -41,7 +41,7 @@ def parse(file, parse_times = PARSE_FULL):
                     times[name] = time
             continue
         # nothing else we know about, ignore
-        print("Ignoring line",line)
+        print("Ignoring line",line,"(in commit {})".format(commit))
     # end of file. previous commit, if any, is done now.
     if commit is not None:
         yield Result(commit, times)
-- 
GitLab