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