diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d4b55529d40e22d86a86be58fe052b000ffe0a94..83071d06d9b2e82a68193efee939127cbcb2c590 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