aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile19
1 files changed, 18 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index afaa48463..c2d6e540c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -87,7 +87,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
output-modulo-time interactive micromega $(COMPLEXITY) modules stm
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
PREREQUISITELOG = prerequisite/admit.v.log \
prerequisite/make_local.v.log prerequisite/make_notation.v.log
@@ -151,6 +151,7 @@ summary:
$(call summary_dir, "IDE tests", ide); \
$(call summary_dir, "VI tests", vio); \
$(call summary_dir, "Coqchk tests", coqchk); \
+ $(call summary_dir, "Coq makefile", coq-makefile); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -481,3 +482,19 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
echo " $<...Error!"; \
fi; \
} > "$@"
+
+coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
+
+coq-makefile/%.log : coq-makefile/%/run.sh
+ @echo "TEST coq-makefile/$*"
+ $(HIDE)(\
+ cd coq-makefile/$* && \
+ ./run.sh 2>&1; \
+ if [ $$? = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error!"; \
+ fi; \
+ ) > "$@"