diff options
| author | Vincent Laporte | 2018-10-08 13:55:18 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-12-10 15:03:17 +0000 |
| commit | 9cdb9e97985598bd28e31af9e4cb23ea9776626c (patch) | |
| tree | b7169c8ab1b44e96aa6b5258bd15d540d0645255 | |
| parent | 21bac03b0997cd79ddf6a8a9b31ee4d8ee63f50a (diff) | |
[test-suite] Fail when the checker fails
| -rw-r--r-- | test-suite/Makefile | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index b764a3d358..9d2277c37e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -329,7 +329,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ - echo " $<...could not be checked" ; \ + echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" @@ -355,7 +355,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ - echo " $<...could not be checked" ; \ + echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" @@ -379,7 +379,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ - echo " $<...could not be checked" ; \ + echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" |