--- a/Admin/isatest-check Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: sends email for failed tests, checks for error.log,
-# generates development snapshot if test ok
-
-## global settings
-. ~/admin/isatest-settings
-
-# produce empty list for patterns like isatest-*.log if no
-# such file exists
-shopt -s nullglob
-
-# mail program
-MAIL=$HOME/bin/pmail
-
-# tmp file for sending mail
-TMP=/tmp/isatest-makedist.$$
-
-export DISTPREFIX
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- 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
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-## main
-
-# check if tests are still running, wait for them a couple of hours
-i=0
-while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do
- sleep 3600
- let "i = i+1"
-done
-
-FAIL=0
-
-# still running -> give up
-if [ -n "$(ls $RUNNING)" ]; then
- echo "Giving up waiting for test to finish at $(date)." > $TMP
- echo >> $TMP
- echo "Sessions still running:" >> $TMP
- echo "$(ls $RUNNING)" >> $TMP
- echo >> $TMP
- echo "Attaching all error logs collected so far." >> $TMP
- echo >> $TMP
-
- if [ -e $ERRORLOG ]; then
- cat $ERRORLOG >> $TMP
- fi
-
- echo "Have a nice day," >> $TMP
- echo " isatest" >> $TMP
-
- for R in $MAILTO; do
- LOGS=$ERRORDIR/isatest*.log
- $MAIL "isabelle test taking too long" $R $TMP $LOGS
- done
-
- rm $TMP
-
- FAIL=1
-elif [ -e $ERRORLOG ]; then
- # no tests running, check if there were errors
- cat $ERRORLOG > $TMP
- echo "Have a nice day," >> $TMP
- echo " isatest" >> $TMP
-
- for R in $MAILTO; do
- LOGS=$ERRORDIR/isatest*.log
- $MAIL "isabelle test failed" $R $TMP $LOGS
- done
-
- rm $TMP
-fi
-
-# generate development snapshot page only for successful tests
-# (failures in experimental sessions ok)
-if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
- (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
- echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
-fi
-
-exit 0
-## end