# HG changeset patch
# User kleing
# Date 1223417022 -7200
# Node ID a30b9cf3502ea4bc03f73be1a06b9f9b0742b89e
# Parent  42297ae4df4706133aae3789dc28544aec6e0a39
leave a log message when no snapshot is generated

diff -r 42297ae4df47 -r a30b9cf3502e Admin/isatest/isatest-check
--- a/Admin/isatest/isatest-check	Tue Oct 07 16:07:59 2008 +0200
+++ b/Admin/isatest/isatest-check	Wed Oct 08 00:03:42 2008 +0200
@@ -48,8 +48,8 @@
 
 # check if tests are still running, wait for them a couple of hours
 i=0
-while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do 
-    sleep 3600
+while [ -n "$(ls $RUNNING)" -a $i -lt 40 ]; do 
+    sleep 900
     let "i = i+1"
 done
 
@@ -99,6 +99,8 @@
 if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
   (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
   echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
+else
+  echo "$(date) $HOSTNAME $PRG: test failures, no web snapshot generated." >> $MASTERLOG
 fi
 
 exit 0