From 8ee0c8fad103366f02b24eb912cdfaf9cb31fc65 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 26 Nov 2020 09:01:22 +0100
Subject: [ci] interval, disable native-compute

---
 dev/ci/ci-interval.sh | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/ci/ci-interval.sh b/dev/ci/ci-interval.sh
index 1e89aac629..fe7b3f9fbe 100755
--- a/dev/ci/ci-interval.sh
+++ b/dev/ci/ci-interval.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download interval
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/interval" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
-- 
cgit v1.2.3