--- a/Admin/isatest-makedist Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
-
-## global settings
-. ~/admin/isatest-settings
-
-TMP=/tmp/isatest-makedist.$$
-MAIL=$HOME/bin/pmail
-
-MAKEDIST=$HOME/bin/makedist
-MAKEALL=$HOME/bin/isatest-makeall
-TAR=gtar
-CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
-
-SSH="ssh -f"
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " Build distribution and run isatest-make for lots of platforms."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-## main
-
-# cleanup old error log and test-still-running files
-rm -f $ERRORLOG
-rm -f $ERRORDIR/isatest-*.log
-rm -f $RUNNING/*.runnning
-
-export DISTPREFIX
-export CVS2CL
-
-DATE=$(date "+%Y-%m-%d")
-DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
-
-echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
-
-echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
-rm -rf $DISTPREFIX >> $DISTLOG 2>&1
-
-echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
-rm -rf $HOME/isabelle-*
-
-echo "### building distribution" >> $DISTLOG 2>&1
-mkdir -p $DISTPREFIX
-$MAKEDIST - >> $DISTLOG 2>&1
-
-if [ $? -ne 0 ]
-then
- 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
-
- echo "Could not build isabelle distribution. Log file available at" > $TMP
- echo "$HOSTNAME:$DISTLOG" >> $TMP
-
- for R in $MAILTO; do
- $MAIL "isabelle dist build failed" $R $TMP
- done
-
- rm $TMP
-
- exit 1
-fi
-
-cd $DISTPREFIX >> $DISTLOG 2>&1
-$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
-
-echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
-
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
-
-
-## spawn test runs
-
-$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
-# give test some time to copy settings and start
-sleep 5
-$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-poly-e"
-sleep 5
-$SSH atbroy10 "$MAKEALL $HOME/settings/at-sml-dev"
-sleep 5
-$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly-e"
-sleep 5
-$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"
-sleep 5
-$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-e"
-
-echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
-
-gzip -f $DISTLOG
-
-## end