diff options
Diffstat (limited to 'tests')
| -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 |