aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2003-02-03 10:11:32 +0000
committerfilliatr2003-02-03 10:11:32 +0000
commitbd3a27df00d1c2fd22cb6d87b835f56a70b43b6f (patch)
treed9e00b1255265eebeb3b3950922897a50652e43b
parent47f5a984f923aa2e1e95ab16d6962d19b2bb5c52 (diff)
make check utilise toujours le Coq local
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3654 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index c93b546cd4..c5f1077acd 100644
--- a/Makefile
+++ b/Makefile
@@ -462,7 +462,8 @@ clean::
###########################################################################
check:: world
- cd test-suite; ./check -$(BEST) | tee check.log
+ cd test-suite; \
+ env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log
if grep -F 'Error!' test-suite/check.log ; then false; fi
###########################################################################