From 787c4583d685e4059c2a08cdb9fe0bbfa99e255e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 14 Nov 2020 12:25:10 +0100
Subject: [CI] Deactivate native-compiler for a few tests that fail with it

---
 test-suite/Makefile | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 279f32c903..6a7cc0428c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -252,7 +252,12 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  (echo "\
+	     bugs/closed/bug_3783.v \
+	     bugs/closed/bug_4157.v \
+	     bugs/closed/bug_5127.v \
+	   " | grep -q "$<") && no_native="-native-compiler no"; \
+	  $(coqc) $$no_native "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
-- 
cgit v1.2.3