--- 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