From b832b0e511cb33e154e4eb145e3046f626f06e57 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Jul 2005 11:02:21 +0000
Subject: [PATCH] do_tests.sh now returns with an error if one of the
 compilations fail

---
 helm/matita/scripts/do_tests.sh | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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
 
-- 
2.39.2