diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8fc6ae8386ea01379f02a56bb06d4438fbbce909..8e82fc715fe3aba030ed7dba48d010ea4911b6c0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -16,7 +16,7 @@ variables: cache: key: "$CI_JOB_NAME" paths: - - opamroot/ + - _opam/ only: - /^master/@iris/iris - /^ci/@iris/iris