From 9cdb9e97985598bd28e31af9e4cb23ea9776626c Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 8 Oct 2018 13:55:18 +0000
Subject: [test-suite] Fail when the checker fails

---
 test-suite/Makefile | 6 +++---
 1 file 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"
-- 
cgit v1.2.3