From fa765186bff18eefc98b3c0ecce5a17a5b941b17 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Sep 2018 08:45:17 +0200
Subject: [PATCH] dont share cache with other branch
---
.gitlab-ci.yml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index af6ccd96..e75417ad 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -14,7 +14,7 @@ variables:
- git clone https://gitlab.mpi-sws.org/FP/iris-ci.git ci -b opam2
- ci/buildjob
cache:
- key: "$CI_JOB_NAME"
+ key: "$CI_JOB_NAME-gen_proofmode_WIP"
paths:
- opamroot/
only:
--
GitLab