aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-03-16 15:33:29 +0100
committerGaëtan Gilbert2020-03-16 15:33:29 +0100
commitd967862488cb10448bf063b7c272929bfb7f8412 (patch)
tree7a39c062aa29c178f4ae5b94973e00ef5472a9bd
parent1f984236f4bdc441b80f19bcc32424a45d8168f3 (diff)
parent9ebe0122113aadf9449719d1b6a6f15a8e530be2 (diff)
Merge PR #11831: [ci] Re-enable VST testing
Reviewed-by: SkySkimmer
-rw-r--r--.gitlab-ci.yml1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8b79dbf810..68bb24ac77 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -697,7 +697,6 @@ 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