# HG changeset patch
# User kleing
# Date 1053267418 -7200
# Node ID 3b7f3eec9684e1ad9a0973f2ef11c3ccad762816
# Parent  fb6040d4bbf8c805552f965c88c434024a94020c
more cleanup

diff -r fb6040d4bbf8 -r 3b7f3eec9684 Admin/isatest-makedist
--- a/Admin/isatest-makedist	Sun May 18 16:15:01 2003 +0200
+++ b/Admin/isatest-makedist	Sun May 18 16:16:58 2003 +0200
@@ -20,7 +20,8 @@
 
 LOGPREFIX=$HOME/log
 MASTERLOG=$LOGPREFIX/isatest.log
-ERRORLOG=$HOME/var/error.log
+ERRORDIR=$HOME/var
+ERRORLOG=$ERRORDIR/error.log
 RUNNING=$HOME/var/running
 DISTPREFIX=$HOME/isadist
 MAKEDIST=$HOME/bin/makedist
@@ -53,6 +54,7 @@
 
 # cleanup old error log and test-still-running files
 rm -f $ERRORLOG
+rm -f $ERRORDIR/isatest-*.log
 rm -f $RUNNING/*.runnning
 
 export DISTPREFIX
@@ -81,7 +83,7 @@
     echo "$HOSTNAME:$DISTLOG" >> $TMP
 
     for R in $MAILTO; do
-	$MAIL "isabelle dist build failed" $R $TMP
+        $MAIL "isabelle dist build failed" $R $TMP
     done
 
     rm $TMP