diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 46f5c7fa5197144bab75fce69943332bc02f284e..2bf249f936cecae3cec908e76beaa72d54ec2af0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -21,8 +21,7 @@ iris-coq8.6: - opamroot/ only: - master - - ci - - timing + - /^ci/ artifacts: paths: - build-time.txt