aboutsummaryrefslogtreecommitdiff
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorxclerc2013-09-20 13:28:06 +0000
committerxclerc2013-09-20 13:28:06 +0000
commita2bb6f5358df6be7f1089a1a06feaf42a6c81257 (patch)
treeb9b1526f56b675e7f225656439aa022e973bd906 /test-suite/Makefile
parentf361ba32a28796514b8d3469c7bee3f43ad61fc1 (diff)
Fix name clash in "failure/inductive.v".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile32
1 files changed, 1 insertions, 31 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 29c211de1b..5d1f822363 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 bugs/closed/shouldsucceed bugs/closed/shouldfail
+ bugs/closed
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
interactive micromega $(COMPLEXITY) modules
@@ -197,36 +197,6 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
fi; \
} > "$@"
-# Closed bugs that should succeed
-$(addsuffix .log,$(wildcard bugs/closed/shouldsucceed/*.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 fail
-$(addsuffix .log,$(wildcard bugs/closed/shouldfail/*.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; \
- } > "$@"
-
#######################################################################
# Other generic tests
#######################################################################