diff options
| author | coqbot-app[bot] | 2020-11-20 21:11:18 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 21:11:18 +0000 |
| commit | 87a59a875b0945fa7976fd16b17a2ff5dd015402 (patch) | |
| tree | 38359d370f084aad4f1acc1ab254822e48901661 /test-suite/Makefile | |
| parent | 1a97ab1856ff8a855645d31e5b2bf665f666ca97 (diff) | |
| parent | c95512bc5716fc477948ae5e4947afe9dca2976d (diff) | |
Merge PR #13352: Configure default value of -native-compiler
Reviewed-by: erikmd
Reviewed-by: silene
Ack-by: mattam82
Ack-by: Blaisorblade
Ack-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer
Ack-by: ejgallego
Diffstat (limited to 'test-suite/Makefile')
| -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"; \ |