Admin/isatest-makeall
changeset 14433 f25291a96e17
parent 14280 d7c3691008f9
child 14981 e73f8140af78
--- a/Admin/isatest-makeall	Thu Mar 04 15:49:42 2004 +0100
+++ b/Admin/isatest-makeall	Fri Mar 05 07:46:07 2004 +0100
@@ -116,7 +116,6 @@
         # test log and cleanup
         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
         gzip -f $TESTLOG
-        rm -rf $HOME/isabelle-$SHORT
     else
         # test log
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1