# 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