From 4d81d151029ef9bc4daadd36b28db70d12a87b56 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jul 2016 11:27:33 +0200
Subject: [PATCH] make the extract script work better

---
 benchmark/gitlab-extract.py | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py
index 8be4a51da..5e9db68f8 100755
--- a/benchmark/gitlab-extract.py
+++ b/benchmark/gitlab-extract.py
@@ -61,9 +61,8 @@ for commit in parse_log.parse_git_commits(args.commits):
         # no build
         continue
     build = first(sorted(builds.json(), key = lambda b: -int(b['id'])))
-    assert build is not None
-    if build['status'] == 'failed':
-        # build failed
+    if build is None or build['status'] == 'failed':
+        # build failed (or missing...??)
         continue
     if build['status'] == 'running':
         # build still running, don't fetch this or any later commit
-- 
GitLab