# HG changeset patch
# User kleing
# Date 1053268158 -7200
# Node ID afeaca7d943aeb55f1ac28c8c334f844d908686e
# Parent  3b7f3eec9684e1ad9a0973f2ef11c3ccad762816
attach log files

diff -r 3b7f3eec9684 -r afeaca7d943a Admin/isatest-check
--- a/Admin/isatest-check	Sun May 18 16:16:58 2003 +0200
+++ b/Admin/isatest-check	Sun May 18 16:29:18 2003 +0200
@@ -10,6 +10,9 @@
 # source bashrc, we're called by cron
 . ~/.bashrc
 
+# produce empty list for patterns like isatest-*.log if no 
+# such file exists 
+shopt -s nullglob
 
 ## global settings
 
@@ -90,8 +93,8 @@
     echo "Have a nice day," >> $TMP
     echo "  isatest" >> $TMP
 
-    cd $ERRORDIR
     for R in $MAILTO; do
+        LOGS=$ERRORDIR/isatest*.log
         $MAIL "isabelle test failed" $R $TMP *.log
     done