From a35e41df73ebfa5c1024213012e06fc2c731278a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Sep 2020 17:46:22 +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 ebb60f3..0c3f452 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,7 +16,7 @@ variables:
cache:
key: "$CI_JOB_NAME"
paths:
- - opamroot/
+ - _opam/
only:
- master
- /^ci/
--
GitLab