From b73581dbc9c7b75a2f076c254502b7b9ad944544 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Sep 2020 18:14:30 +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 1dad2e95..27839b38 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,7 +16,7 @@ variables:
cache:
key: "$CI_JOB_NAME-weak_mem"
paths:
- - opamroot/
+ - _opam/
only:
- /^master/
- /^ci/
--
GitLab