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