aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-01-29 15:42:59 +0100
committerEmilio Jesus Gallego Arias2019-01-29 15:42:59 +0100
commit966efd33caa990839657b485bc3eb82de332d799 (patch)
tree329845c03d3ac8058c6452afc95a082016cc0a55
parent67d0d038d1a2fba80a086c1c2096cfa3166ef362 (diff)
[test-suite] Display full paths on CHECK.
This makes the display consistent wrt `TEST`: ``` TEST failure/Case7.v CHECK Case7 ``` vs ``` TEST failure/Case7.v CHECK failure/Case7.v ```
-rw-r--r--test-suite/Makefile8
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index d33ae57ae2..f393d3ec98 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -307,7 +307,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
echo " $<...correctly prepared" ; \
fi; \
} > "$@"
- @echo "CHECK $(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)
@@ -326,7 +326,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v
$(FAIL); \
fi; \
} > "$@"
- @echo "CHECK $(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=$$?; \
@@ -353,7 +353,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
$(FAIL); \
fi; \
} > "$@"
- @echo "CHECK $(shell basename $< .v)"
+ @echo "CHECK $<"
$(HIDE){ \
$(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \
if [ $$R != 0 ]; then \
@@ -377,7 +377,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
$(FAIL); \
fi; \
} > "$@"
- @echo "CHECK $(shell basename $< .v)"
+ @echo "CHECK $<"
$(HIDE){ \
$(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \
if [ $$R != 0 ]; then \