--- a/Admin/isatest-makeall Mon Jul 15 10:41:34 2002 +0200
+++ b/Admin/isatest-makeall Mon Jul 15 15:28:51 2002 +0200
@@ -8,7 +8,7 @@
# Send email if it fails.
## global settings
-MAILTO="kleing@in.tum.de test@jflex.de"
+MAILTO="kleing@in.tum.de nipkow@in.tum.de wenzelm@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
LOGPREFIX=~/log
@@ -79,7 +79,7 @@
else
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
FAIL="$FAIL$SHORT "
- LOGS="${LOGS}$HOSTNAME:$TESTLOG\n"
+ LOGS="${LOGS}$HOSTNAME:$TESTLOG "
fi
done
@@ -90,7 +90,7 @@
echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
- echo "$LOGS" >> $TMP
+ for L in $LOGS; do echo "$L" >> $TMP; done
for R in $MAILTO; do
$MAIL "isabelle test failed" $R $TMP
--- a/Admin/isatest-makedist Mon Jul 15 10:41:34 2002 +0200
+++ b/Admin/isatest-makedist Mon Jul 15 15:28:51 2002 +0200
@@ -11,7 +11,10 @@
## global settings
-MAILTO="kleing@in.tum.de test@jflex.de"
+MAILTO="kleing@in.tum.de nipkow@in.tum.de wenzelm@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
+
+TMP=/tmp/isatest-makedist.$$
+MAIL=~/bin/pmail
LOGPREFIX=~/log
MASTERLOG=$LOGPREFIX/isatest.log
@@ -69,17 +72,15 @@
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
+ echo "Could not build isabelle distribution. Log file available at" > $TMP
+ echo "$HOSTNAME:$DISTLOG" >> $TMP
-Could not build isabelle distribution. Log file available at
-
-$HOSTNAME:$DISTLOG
-EOM
+ for R in $MAILTO; do
+ $MAIL "isabelle dist build failed" $R $TMP
done
- # more action here
+ rm $TMP
+
exit 1
fi
@@ -97,7 +98,6 @@
# run tests in parallel on multiprocessor sun
$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"