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