added homepage URL, now we have one

[helm.git] / helm / matita / scripts / do_tests.sh

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index 687cb26d7192e0c3eaced9f933b678a7fce688d3..a195b9cf0ee4ba816e29bbe917e3d2101db7c8de 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -45,11 +45,13 @@ 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"
+    rm $TMP
   else
-    printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n"
+    printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n";
+    rm $TMP
+    exit $RC
   fi
 done
-
-rm $TMP