--- 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
--- a/Admin/isatest-makedist Mon Jun 24 11:59:21 2002 +0200
+++ b/Admin/isatest-makedist Mon Jun 24 16:33:43 2002 +0200
@@ -11,6 +11,8 @@
## global settings
+MAILTO="kleing@in.tum.de test@jflex.de"
+
LOGPREFIX=~/log
MASTERLOG=$LOGPREFIX/isatest.log
DISTPREFIX=~/isadist
@@ -66,6 +68,17 @@
echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+
+ for R in $MAILTO; do
+ mail -t $R <<EOM
+Subject: isabelle dist build failed
+
+Could not build isabelle distribution. Log file available at
+
+$HOSTNAME:$DISTLOG
+EOM
+ done
+
# more action here
exit 1
fi
@@ -83,8 +96,8 @@
## spawn test runs
# run tests in parallel on multiprocessor sun
-$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly"
-$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-sml"
+$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly ~/settings/sun-sml"
+# $SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-sml"
# run tests sequentially on x86
$SSH $AT "$MAKEALL $DISTPREFIX ~/settings/at-poly ~/settings/at-sml"