Admin/isatest-makeall
changeset 13246 e51efc2029e9
parent 13236 568bc754d303
child 13320 2c6ee189ae63
--- a/Admin/isatest-makeall	Mon Jun 24 11:59:21 2002 +0200
+++ b/Admin/isatest-makeall	Mon Jun 24 16:33:43 2002 +0200
@@ -8,6 +8,8 @@
 #              Send email if it fails.
 
 ## global settings
+MAILTO="kleing@in.tum.de test@jflex.de"
+
 LOGPREFIX=~/log
 
 MASTERLOG=$LOGPREFIX/isatest.log
@@ -69,9 +71,19 @@
         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
         mv $DISTPREFIX/Isabelle/etc/settings.save-$SHORT $DISTPREFIX/Isabelle/etc/settings
         gzip -f $TESTLOG
+	rm -rf ~/isabelle-$SHORT
     else
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
 	FAIL="$FAIL$SHORT "
+	for R in $MAILTO; do
+    		mail -t $R <<EOM
+Subject: isabelle test failed
+
+Test for platform $SHORT failed. Log file available at
+
+$HOSTNAME:$TESTLOG
+EOM
+	done
         # more action here
     fi