diff options
| author | Pierre-Marie Pédrot | 2017-08-02 01:26:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 01:27:15 +0200 |
| commit | d3c3859ab6dba6495b13e055917ddf3d95851912 (patch) | |
| tree | 0c3441e9db936865e7e873ac591b9d178fbd3885 | |
| parent | b760af386d3c69c6963231489094685ea2a1e673 (diff) | |
Better test Makefile.
| -rw-r--r-- | tests/Makefile | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tests/Makefile b/tests/Makefile index a48ab0860f..9370b063f8 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,7 +1,12 @@ all: $(patsubst %.v,%.v.log,$(wildcard *.v)) %.v.log: %.v - $(COQBIN)/coqtop -I ../src -Q ../theories Ltac2 < $< 2> $@ + $(COQBIN)/coqtop -batch -I ../src -Q ../theories Ltac2 -lv $< > $@ + if [ $$? = 0 ]; then \ + echo " $<... OK"; \ + else \ + echo " $<... FAIL!"; \ + fi; \ clean: rm -f *.log |