From 8b054d9f209a060325c93c740a6c14e3afbd67b5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Sep 2020 17:45:57 +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 07730bae..12599ed8 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
-- 
GitLab