diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-19 20:41:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-19 20:43:31 +0200 |
| commit | 969e77f88fe2c9d766cd2cf6e6fd7d08719a7cb7 (patch) | |
| tree | 4e2f71e0ebd9a1c1fb58082907c513ebd5a30e80 | |
| parent | fd0fc9a8bd820d9ae1466a941a0a903efb8be7b6 (diff) | |
Do that "make" in test-suite writes failures as a default together
with a more explicit message.
| -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 f333ae63e..083577d60 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -92,7 +92,7 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk .PHONY: all run clean $(SUBSYSTEMS) all: run - $(MAKE) --quiet summary.log + $(MAKE) report run: $(SUBSYSTEMS) bugs: $(BUGS) @@ -151,11 +151,11 @@ summary: } summary.log: - $(SHOW) SUMMARY + $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" report: summary.log - $(HIDE)if grep -F 'Error!' summary.log ; then false; fi + $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### # Regression (and progression) tests |