From d8042e88c2acb75e19e7d70dfd1248b876f9cf2f Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Fri, 16 Sep 2016 11:02:28 +0200
Subject: [PATCH] Try cache only for our vio files
---
.gitlab-ci.yml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 509cadea..98e2c39d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -32,6 +32,9 @@ vio:
cat build-log-vio.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
only:
- master
+ cache:
+ paths:
+ - coq/ra/*.vio
artifacts:
paths:
- coq/ra/build-time-vio.txt
--
GitLab