diff options
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 6efd47afc2..ba591ede20 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -317,8 +317,6 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v echo " $<...correctly prepared" ; \ fi; \ } > "$@" - @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) $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG) |