diff -r b02de2918c59 -r f25291a96e17 Admin/isatest-makeall
--- 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