aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-10 18:22:01 -0400
committerEmilio Jesus Gallego Arias2020-03-10 18:22:01 -0400
commit8b35c0775330711e1c63a7e1d0515052812a9f02 (patch)
treebc971ae2cf52958dcb907bf3a421c0ba1f637414
parent98b25745ab50df8f5f263cd32dbe8525aa525ea8 (diff)
[ci] [gitlab] Move VST to `allow_failure`
VST has been broken for a few days, moving to allow failure.
-rw-r--r--.gitlab-ci.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 68bb24ac77..8b79dbf810 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -697,6 +697,7 @@ library:ci-verdi-raft:
library:ci-vst:
extends: .ci-template-flambda
+ allow_failure: true
# Plugins are by definition the projects that depend on Coq's ML API