diff options
| author | Pierre Roux | 2020-11-14 12:25:10 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-11-20 19:08:08 +0100 |
| commit | 787c4583d685e4059c2a08cdb9fe0bbfa99e255e (patch) | |
| tree | b6a66af14d064482f4134e1cd177fb9a5c4d8fca | |
| parent | 146415fb624c182493d46413d738a3c2c3f47e02 (diff) | |
[CI] Deactivate native-compiler for a few tests that fail with it
| -rw-r--r-- | test-suite/Makefile | 7 |
1 files changed, 6 insertions, 1 deletions
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"; \ |