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