# HG changeset patch
# User kleing
# Date 1053264521 -7200
# Node ID c46ce87960fbd60784a766f2642fa36c3e0d3200
# Parent  55ba81e3502bf9f3ce8e68c0501dad011a0b1fe9
attach log files

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
diff -r 55ba81e3502b -r c46ce87960fb Admin/isatest-makeall
--- a/Admin/isatest-makeall	Sun May 18 15:15:13 2003 +0200
+++ b/Admin/isatest-makeall	Sun May 18 15:28:41 2003 +0200
@@ -14,7 +14,8 @@
 # where the log files are
 LOGPREFIX=$HOME/log
 MASTERLOG=$LOGPREFIX/isatest.log
-ERRORLOG=$HOME/var/error.log
+ERRORDIR=$HOME/var
+ERRORLOG=$ERRORDIR/error.log
 
 # where to put test-is-running files
 RUNNING=$HOME/var/running
@@ -121,13 +122,13 @@
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
 
         # error log
-        echo "Test for platform ${SHORT} failed. Log file available at" >> $ERRORLOG
-        echo "$HOSTNAME:$TESTLOG" >> $ERRORLOG
+        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
         echo "[...]" >> $ERRORLOG
-        tail -3 $L >> $ERRORLOG
+        tail -3 $TESTLOG >> $ERRORLOG
         echo >> $ERRORLOG
 
         FAIL="$FAIL$SHORT "
+        (cd $ERRORDIR; ln -s $TESTLOG)
     fi
 
     rm -f $RUNNING/$SHORT.running