From 969e77f88fe2c9d766cd2cf6e6fd7d08719a7cb7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Apr 2016 20:41:52 +0200 Subject: Do that "make" in test-suite writes failures as a default together with a more explicit message. --- test-suite/Makefile | 6 +++--- 1 file 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 -- cgit v1.2.3