diff options
| author | Enrico Tassi | 2019-02-04 12:55:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-04 12:55:28 +0100 |
| commit | 0be49a49c41e28b2015440723882e0ca15c02d5e (patch) | |
| tree | a16bde40ecba74fee163c9710350f77ff9524095 | |
| parent | 2de5a4b0d4c7ca5c21b2aae44844019f9fbe4e81 (diff) | |
| parent | 966efd33caa990839657b485bc3eb82de332d799 (diff) | |
Merge PR #9426: [test-suite] Fix display of check.
Reviewed-by: gares
| -rw-r--r-- | test-suite/Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 111bd52a33..c55e15858a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,7 +304,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v echo " $<...correctly prepared" ; \ fi; \ } > "$@" - @echo "CHK $(shell basename $< .v)" + @echo "CHECK $<" $(HIDE)$(coqchk) -norec TestSuite.$(shell basename $< .v) > $(shell dirname $<)/$(shell basename $< .v).chk.log 2>&1 ssr: $(wildcard ssr/*.v:%.v=%.v.log) @@ -323,7 +323,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v $(FAIL); \ fi; \ } > "$@" - @echo "CHK $(shell basename $< .v)" + @echo "CHECK $<" $(HIDE){ \ 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=$$?; \ @@ -350,7 +350,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(FAIL); \ fi; \ } > "$@" - @echo "CHK $(shell basename $< .v)" + @echo "CHECK $<" $(HIDE){ \ $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ @@ -374,7 +374,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(FAIL); \ fi; \ } > "$@" - @echo "CHK $(shell basename $< .v)" + @echo "CHECK $<" $(HIDE){ \ $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ |