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