From 966efd33caa990839657b485bc3eb82de332d799 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 29 Jan 2019 15:42:59 +0100 Subject: [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 ``` --- test-suite/Makefile | 8 ++++---- 1 file 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 \ -- cgit v1.2.3