we totally did not record timing in artifacts since we switched to 8.6-only...

f42d7b3e · Ralf Jung · 24e91f98 · f42d7b3e
Commit f42d7b3e authored Feb 16, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

.gitlab-ci.yml .gitlab-ci.yml +3 -0

No files found.
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,3 +19,6 @@ iris-coq8.6:
  - master
  - ci
  - timing
+  artifacts:
+    paths:
+    - build-time.txt