diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d9a22c5cdc..7915cc34fb 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -744,6 +744,7 @@ library:ci-fiat_crypto: library:ci-fiat_crypto_legacy: extends: .ci-template-flambda + allow_failure: true # See https://github.com/coq/coq/wiki/Coq-Call-2020-06-24#adding-back-fiat-crypto-legacy # We cannot use flambda due to # https://github.com/ocaml/ocaml/issues/7842, see |