From 542323df01f3f70f0faeda54a0749e97cecf380f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Apr 2018 17:04:51 +0200
Subject: [PATCH] fix gitlab-extract output if build is still running

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

diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py
index de38705e6..926b06ff0 100755
--- a/benchmark/gitlab-extract.py
+++ b/benchmark/gitlab-extract.py
@@ -114,5 +114,5 @@ for commit in parse_log.parse_git_commits(args.commits):
             found_build = True
             print(" success")
             break
-    if not found_build:
+    if not found_build and not BREAK:
         print(" found no succeessful build")
-- 
GitLab