From 28ddbd0ddef76642bbd8817f28eab2d68cef4758 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Fri, 16 Sep 2016 11:24:04 +0200
Subject: [PATCH] Disable CI vio2vo job for now
---
.gitlab-ci.yml | 1 +
1 file changed, 1 insertion(+)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 98e2c39d..61f334ab 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -50,6 +50,7 @@ vio2vo:
cat build-log-vio2vo.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio2vo.txt
only:
- master
+ allow_failure: true
artifacts:
paths:
- coq/ra/build-time-vio2vo.txt
--
GitLab