diff -r 93769c6c85d7 -r 88a8911bb65d Admin/isatest-check
--- a/Admin/isatest-check	Fri May 09 14:08:04 2003 +0200
+++ b/Admin/isatest-check	Fri May 09 14:15:50 2003 +0200
@@ -4,7 +4,8 @@
 # Author: Gerwin Klein, TU Muenchen
 # License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
-# DESCRIPTION: sends email for failed tests (checks for error.log)
+# DESCRIPTION: sends email for failed tests, checks for error.log,
+#              generates development snapshot if test ok
 
 # source bashrc, we're called by cron
 . ~/.bashrc
@@ -20,11 +21,15 @@
 # canoncical home for all platforms
 HOME=/usr/stud/isatest
 
+# where to find the distribution
+DISTPREFIX=$HOME/isadist
+
 # mail program
 MAIL=$HOME/bin/pmail
 
-# where the error log is
+# where the logs are
 ERRORLOG=$HOME/var/error.log
+MASTERLOG=$HOME/log/isatest.log
 
 # where the test-still-running files are
 RUNNING=$HOME/var/running
@@ -42,7 +47,8 @@
   echo
   echo "Usage: $PRG"
   echo
-  echo "   sends email for failed tests, checks for error.log."
+  echo "   sends email for failed tests, checks for error.log,"
+  echo "   generates development snapshot if test ok."
   echo "   To be called by cron."
   echo
   exit 1
@@ -91,5 +97,9 @@
     exit 1
 fi
 
+# generate development snapshot page only for successful tests
+(cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
+echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
+
 exit 0
 ## end