'make check' echoue si au moins un test echoue.

Les distributions binaires ne peuvent etre faites que si 'make check' reussit.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2751 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 24 insertions, 11 deletions

diff --git a/Makefile b/Makefile
index 3282b3f915..48438d16bf 100644
--- a/Makefile
+++ b/Makefile
@@ -378,8 +378,12 @@ clean::
 # tests
 ###########################################################################
 
-check:: $(BESTCOQTOP)
-	cd test-suite; ./check -$(BEST)
+check.log: world
+	cd test-suite; ./check -$(BEST) > check.log
+
+check:: check.log
+	cat check.log
+	grep -F 'Error!' check.log
 
 ###########################################################################
 # theories and states
diff --git a/distrib/Makefile b/distrib/Makefile
index 9c0c225d85..aecc992347 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -86,15 +86,15 @@ arch-rpm: ${COQRPMPACKAGE}.${ARCH}.rpm
 test:
 	cp ${COQPACKAGE}.tar.gz tmp.tar.gz
 	gunzip tmp.tar.gz
-	@echo Trying "make world"
+	@echo Trying "make world check"
 	- rm -rf ${COQPACKAGE}
 	tar xf tmp.tar
 	(cd ${COQPACKAGE};\
 	configure -local -opt -emacs emacs;\
-	make world >& log.world;\
+	make world check >& log.world;\
 	if [ $$? = 0 ];\
-	then echo make world succeeded;\
-	else echo make world failed; exit 1;\
+	then echo '"make world check" succeeded';\
+	else echo '"make world check" failed'; exit 1;\
 	fi)
 	rm tmp.tar
 	@echo "Compilation succeeded"
@@ -127,7 +127,7 @@ arch-tar-gz: ${COQPACKAGE}.tar.gz
 	gunzip -c $(DISTRIBDIR)/${COQPACKAGE}.tar.gz | tar xf -;\
 	cd ${COQPACKAGE};\
 	./configure -bindir /usr/local/bin -libdir /usr/local/lib/coq -mandir /usr/local/man -emacs emacs -emacslib /usr/local/lib/emacs/site-lisp -opt;\
-	make world;\
+	make world check;\
 	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
 	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install)
 	$(MAKE) arch-tar-gz-final
@@ -141,7 +141,7 @@ win: ${COQPACKAGE}.tar.gz
 	gunzip -c $(DISTRIBDIR)/${COQPACKAGE}.tar.gz | tar xf -;\
 	cd ${COQPACKAGE};\
 	./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs;\
-	make world;\
+	make world check;\
 	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
 	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install;\
 	cd ${ARCHBUILDROOT}/buildroot;\
@@ -318,8 +318,8 @@ prep-deb: ${COQDEBORIG}.tar.gz ${COQPACKAGE}.tar.gz
 
 deb: prep-deb
 	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee ../../deb.log
-	lintian deb_build/${COQDEBCHANGES} || true
+	(lintian deb_build/${COQDEBCHANGES} | tee lintian.log) || true
 
 deb-sign: prep-deb
 	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot 2>&1 | tee ../../deb.log
-	lintian deb_build/${COQDEBCHANGES} || true
+	(lintian deb_build/${COQDEBCHANGES} | tee lintian.log) || true
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
index b504dd070d..069a81c205 100644
--- a/distrib/RH/do_build
+++ b/distrib/RH/do_build
@@ -1,2 +1,2 @@
 ./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt         # Need ocamlc.opt and ocamlopt.opt
-make world       # Use native coq to compile theories
+make world check      # Use native coq to compile theories
diff --git a/distrib/debian/changelog b/distrib/debian/changelog
index 501b6e349f..9d460a24a3 100644
--- a/distrib/debian/changelog
+++ b/distrib/debian/changelog
@@ -1,3 +1,9 @@
+coq (7.3-1) unstable; urgency=low
+
+  * New upstream version.
+ 
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Wed, 22 May 2002 14:48:21 +0200
+
 coq (7.2-9) unstable; urgency=low
   * ocamlc.opt completely broken on powerpc. Added a special case in
     "rules" for using only bytecode.
diff --git a/distrib/debian/control b/distrib/debian/control
index 4978041164..7baddee0de 100644
--- a/distrib/debian/control
+++ b/distrib/debian/control
@@ -14,3 +14,5 @@ Description: a proof assistant for higher-order logic.
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
  specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+
diff --git a/distrib/debian/rules b/distrib/debian/rules
index 72835d099e..d2b7b3b4e4 100755
--- a/distrib/debian/rules
+++ b/distrib/debian/rules
@@ -45,6 +45,7 @@ build-stamp:
 	    && echo Coq was built in bytecode instead); \
 	else ${MAKE} world; \
 	fi
+	${MAKE} check
 	touch build-stamp
 
 clean: