From cbcf0903ee3b221acd34d0daea88987a96225df6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Feb 2016 08:25:06 +0100
Subject: [PATCH] try to get build times as an artifact

---
 .gitlab-ci.yml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ac6257df8..40952712c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -4,4 +4,7 @@ buildjob:
   tags:
   - coq
   script:
-  - make -j4 TIMED=y
+  - make -j8 TIMED=y | tee /dev/stdout | egrep "[a-zA-Z0-9-_/]+ \(user: [0-9]" > build-time.txt
+  artifacts:
+    paths:
+    - build-time.txt
-- 
GitLab