diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7b1a6642db0d34ac5f7bc9af6867203f3dcbcd6e..be9419407a4194c261532899beca4036aad470ac 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -20,9 +20,7 @@ lrust-coq8.6: - opamroot/ only: - master - - ci - - /^ralf/ci// - - jh/undiscriminated_hintdb + - /^ci/ artifacts: paths: - build-time.txt