From 77852d7f3b993c6209b93e3a10d813a03fe8fd0f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 Feb 2020 15:14:56 +0100
Subject: [PATCH] play with CI config
---
.gitlab-ci.yml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index aae3367f7..2b55458e4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,7 +18,7 @@ variables:
paths:
- opamroot/
only:
- - master@iris/iris
+ - /^master/@iris/iris
- /^ci/@iris/iris
except:
- triggers
--
GitLab