diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 509cadeac4a28f3b3cd18c49ec7727f546b55773..98e2c39dfdd3a4360290d8831af934fe812c2eed 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