--- 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
--- a/Admin/isatest-makedist Fri May 09 14:08:04 2003 +0200
+++ b/Admin/isatest-makedist Fri May 09 14:15:50 2003 +0200
@@ -92,9 +92,6 @@
cd $DISTPREFIX >> $DISTLOG 2>&1
$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
-echo "### generating development snapshot web page" >> $DISTLOG 2>&1
-(cd $HOME/devel-page; make)
-
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
gzip -f $DISTLOG