From ffa867c4b33c7b52e72ce005cd8183d8e51f310b Mon Sep 17 00:00:00 2001
From: glondu
Date: Sat, 10 Apr 2010 22:53:52 +0000
Subject: Run parallelized test-suite in "check" target of main Makefile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12926 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 0ac6b1f39b..8ded28301b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -358,10 +358,12 @@ validate:: $(BESTCHICKEN) $(ALLVO)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
+MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE)
+
 check:: world
-	cd test-suite; \
-	env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log
-	if grep -F 'Error!' test-suite/check.log ; then false; fi
+	$(MAKE) $(MAKE_TSOPTS) clean
+	$(MAKE) $(MAKE_TSOPTS) all
+	$(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi
 
 ##################################################################
 # partial targets: 1) core ML parts
-- 
cgit v1.2.3