diff -r 55ba81e3502b -r c46ce87960fb Admin/isatest-check
--- a/Admin/isatest-check	Sun May 18 15:15:13 2003 +0200
+++ b/Admin/isatest-check	Sun May 18 15:28:41 2003 +0200
@@ -28,7 +28,8 @@
 MAIL=$HOME/bin/pmail
 
 # where the logs are
-ERRORLOG=$HOME/var/error.log
+ERRORDIR=$HOME/var
+ERRORLOG=$ERRORDIR/error.log
 MASTERLOG=$HOME/log/isatest.log
 
 # where the test-still-running files are
@@ -89,8 +90,9 @@
     echo "Have a nice day," >> $TMP
     echo "  isatest" >> $TMP
 
+    cd $ERRORDIR
     for R in $MAILTO; do
-        $MAIL "isabelle test failed" $R $TMP
+        $MAIL "isabelle test failed" $R $TMP *.log
     done
 
     rm $TMP