diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 07730bae9462e51f29dc0a88800d18d003728ed6..12599ed84672cd6ba41d89b6f223534841ccb180 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/stdpp - /^ci/@iris/stdpp