From d2f2c10535a8eb616d9b3b0de51e7f340988d433 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Sep 2020 18:14:19 +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 256db65a..b32e10da 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