record timing information in artifact

e8e97884 · Ralf Jung · 25387faa · e8e97884
Commit e8e97884 authored 8 years ago by Ralf Jung
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -36,3 +36,6 @@ stdpp-coq8.6:
  - master
  - ci
  - timing
+  artifacts:
+    paths:
+    - build-time.txt