From 89c7574ce888c4f8ee619b12e2182154ffb3a24a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Apr 2021 17:24:01 +0200
Subject: CI-paramcoq: Re-enable native

It's an issue in paramcoq's test suite, which doesn't respect
COQEXTRAFLAGS and so will be handled upstream
(https://github.com/coq-community/paramcoq/pull/66)
---
 dev/ci/ci-paramcoq.sh | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index 1b2d6a73a2..d2e0ee89bf 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,7 +5,4 @@ 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