diff options
| author | Enrico Tassi | 2019-03-13 14:51:41 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-13 14:51:41 +0100 |
| commit | 27ab0d69e87fa3ce414cdaa205f7f6266693e263 (patch) | |
| tree | d023ceaefd94c47cbf3ea11afec10273984caf9a | |
| parent | 425c02cb6dc4578aebc62ff94c656a904e5d6299 (diff) | |
| parent | 0e2bb26240b785d4ca618cfbc042b13c613fa78f (diff) | |
Merge PR #9736: Don't coqchk the test suite prerequisites
Reviewed-by: gares
| -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) |