From f34946ecfb0ea2c75337369f3e41e9562be0d84b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 27 Dec 2014 12:02:18 +0100
Subject: include test-suite/coqchk in the summary log

---
 test-suite/Makefile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 45a2e20464..d5adc4e5f9 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -141,6 +141,7 @@ summary:
 	  $(call summary_dir, "STM tests", stm); \
 	  $(call summary_dir, "IDE tests", ide); \
 	  $(call summary_dir, "VI tests", vi); \
+	  $(call summary_dir, "Coqchk tests", coqchk); \
 	  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`; \
-- 
cgit v1.2.3