aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b53f6e4a3d..d4ffe0c283 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -687,6 +687,7 @@ library:ci-math-comp:
library:ci-sf:
extends: .ci-template
+ allow_failure: true # Waiting for integration of the fix for #10476
library:ci-stdlib2:
extends: .ci-template-flambda