diff -r 3852929a8d1d -r d2fd7deceaa6 Admin/isatest-check
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest-check	Fri May 09 11:47:29 2003 +0200
@@ -0,0 +1,93 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# DESCRIPTION: sends email for failed tests (checks for error.log)
+
+# source bashrc, we're called by cron
+. ~/.bashrc
+
+
+## global settings
+
+# send mail to:
+MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
+
+ADMIN="kleing@in.tum.de"
+
+# canoncical home for all platforms
+HOME=/usr/stud/isatest
+
+# mail program
+MAIL=$HOME/bin/pmail
+
+# where the error log is
+ERRORLOG=$HOME/var/error.log
+
+# where the test-still-running files are
+RUNNING=$HOME/var/run/
+
+# tmp file for sending mail
+TMP=/tmp/isatest-makedist.$$
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG"
+  echo
+  echo "   sends email for failed tests, checks for error.log."
+  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 to finish for max 10h
+i=0
+while [ -n $(ls $RUNNING) -a $((i < 10)) ]; do 
+    sleep 3600
+    $((i = i+1))
+done
+
+# still running -> give up
+if [ -n $(ls $RUNNING) ]; then
+    echo "giving up waiting for test to finish at $(date)" > $TMP
+    echo >> $TMP
+    echo "Have a nice day," >> $TMP
+    echo "  isatest" >> $TMP
+
+    for R in $ADMIN; do
+        $MAIL "isabelle taking to long" $R $TMP
+    done
+    
+    exit 1
+fi
+
+# no tests running, check if there were errors
+if [ -e $ERRORLOG ]; then
+  cat $ERRORLOG > $TMP
+	echo "Have a nice day," >> $TMP
+	echo "  isatest" >> $TMP
+
+  for R in $MAILTO; do
+	    $MAIL "isabelle test failed" $R $TMP
+	done
+
+	rm $TMP
+fi
+
+## end