diff options
| author | Gaëtan Gilbert | 2020-04-13 16:41:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 16:41:03 +0200 |
| commit | b8fcbecf8e1b96dcb47f15ac7573197de43f0bdb (patch) | |
| tree | 58555d9bcf80eba6b0efe56ef6ffd5ba3a59cd28 | |
| parent | 0beca74bc90cef03d779a8e4f8668335c9c37716 (diff) | |
| parent | cb35474d6d55f353745c0cd470d76a72c352c9d2 (diff) | |
Merge PR #12081: [test-suite] Remove deprecated -I option of coqchk in Makefile
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/Makefile | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index eade52b6eb..954a922c8c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -354,8 +354,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primit } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ - $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ + $(coqchk) -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -381,7 +380,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -405,7 +404,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ |