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 687cb26d7192e0c3eaced9f933b678a7fce688d3..970828a6478dfff6a222963456ec6394c22ae0f4 100755 (executable)
--- 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