Admin/isatest-makedist
changeset 13246 e51efc2029e9
parent 13237 493d61afa731
child 13359 982827aacb39
--- 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"