From 0496f86a59b90bb4233a8d14f8b445d9cc4f26a9 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 29 Sep 2020 17:45:34 +0200 Subject: [PATCH] update CI config --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8fc6ae838..8e82fc715 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 -- GitLab