From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Jul 2005 11:02:21 +0000 (+0000)
Subject: do_tests.sh now returns with an error if one of the compilations fail
X-Git-Tag: V_0_7_2~182
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b832b0e511cb33e154e4eb145e3046f626f06e57;p=helm.git

do_tests.sh now returns with an error if one of the compilations fail
---

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index 687cb26d7..970828a64 100755
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -45,10 +45,12 @@ for T in $TODO; do
   fi
   $CLEANER $T 1>/dev/null 2>/dev/null
   /usr/bin/time --quiet -o $TMP -f "%E  %U  %S" $COMPILER $T >> $LOGFILE 2>&1
-  if [ $? = 0 ]; then
+  RC=$?;
+  if [ $RC = 0 ]; then
     printf "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA\n"
   else
-    printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n"
+    printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n";
+    exit $RC
   fi
 done