From 48d1bf37f32df48984ee83084b8ca6aa0bd4c68a Mon Sep 17 00:00:00 2001
From: xclerc
Date: Fri, 20 Sep 2013 12:28:58 +0000
Subject: Execute tests from the "bugs/closed" directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16794 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/Makefile | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 355ea2d024..29c211de1b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -65,7 +65,7 @@ log_intro = "==========> TESTING $(1) <=========="
 COMPLEXITY := $(if $(bogomips),complexity)
 
 BUGS := bugs/opened/shouldnotfail bugs/opened/shouldnotsucceed \
-  bugs/closed/shouldsucceed bugs/closed/shouldfail
+  bugs/closed bugs/closed/shouldsucceed bugs/closed/shouldfail
 
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   interactive micromega $(COMPLEXITY) modules
@@ -182,6 +182,21 @@ $(addsuffix .log,$(wildcard bugs/opened/shouldnotfail/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
+# Closed bugs that should succeed
+$(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
+	@echo "TEST      $<"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  $(command) "$<" 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error! (bug seems to be opened, please check)"; \
+	  fi; \
+	} > "$@"
+
 # Closed bugs that should succeed
 $(addsuffix .log,$(wildcard bugs/closed/shouldsucceed/*.v)): %.v.log: %.v
 	@echo "TEST      $<"
-- 
cgit v1.2.3