From e8e97884666778e204bd34bd118766ea9e4b54e2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Feb 2017 22:50:03 +0100
Subject: [PATCH] record timing information in artifact

---
 .gitlab-ci.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6ce0d7ed..ba435ebe 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -36,3 +36,6 @@ stdpp-coq8.6:
   - master
   - ci
   - timing
+  artifacts:
+    paths:
+    - build-time.txt
-- 
GitLab