diff options
| author | Gaëtan Gilbert | 2019-03-11 13:52:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-11 13:52:21 +0100 |
| commit | 0e2bb26240b785d4ca618cfbc042b13c613fa78f (patch) | |
| tree | b2d558d2bf34f0bc731062a71b46c9f7f3e43420 /test-suite | |
| parent | 74534f84a782f5de740c52cb97b3ca3a02eb6aa2 (diff) | |
Don't coqchk the test suite prerequisites
This causes the makefile to break due to dependencies when it fails,
and it's not worth adding a whole mess of code to catch the failure
for these files.
Diffstat (limited to 'test-suite')
| -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) |