From d1ed4cb31076dedbfb19c2023915b4976dbc07c4 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Thu, 16 Feb 2017 22:56:11 +0100
Subject: [PATCH] Track timing artifacts.

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

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d4b55529..83071d06 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,3 +19,6 @@ gps-coq8.6:
   - master
   - /^bench-.*$/
   - opam-ci
+   artifacts:
+     paths:
+     - build-time.txt
\ No newline at end of file
-- 
GitLab