From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Jul 2005 11:34:41 +0000 (+0000)
Subject: Used to left temporary file if something failed.
X-Git-Tag: V_0_7_2~177
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e0bd11e3e344cd86089dadf6f654ce685139802;p=helm.git

Used to left temporary file if something failed.
---

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index 970828a64..a195b9cf0 100755
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -48,10 +48,10 @@ for T in $TODO; do
   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";
+    rm $TMP
     exit $RC
   fi
 done
-
-rm $TMP