From 6c72eb81734451944a9abceedac5de504cc4d81b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 1 Apr 2021 15:16:16 +0200
Subject: [ci] Disable native compilation for paramcoq

Paramcoq is typically flaky on our worker configuration, c.f.
https://gitlab.com/coq/coq/-/jobs/1144081161
---
 dev/ci/ci-paramcoq.sh | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index d2e0ee89bf..1b2d6a73a2 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,4 +5,7 @@ ci_dir="$(dirname "$0")"
 
 git_download paramcoq
 
+# Typically flaky on our worker configuration
+# https://gitlab.com/coq/coq/-/jobs/1144081161
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples)
-- 
cgit v1.2.3