send email plaform independently
authorisatest
Tue Jul 09 11:46:36 2002 +0200 (2002-07-09)
changeset 133202c6ee189ae63
parent 13319 23de7b3af453
child 13321 70a5d5fc081a
send email plaform independently
Admin/isatest-makeall
Admin/pmail
     1.1 --- a/Admin/isatest-makeall	Tue Jul 09 10:44:53 2002 +0200
     1.2 +++ b/Admin/isatest-makeall	Tue Jul 09 11:46:36 2002 +0200
     1.3 @@ -14,6 +14,10 @@
     1.4  
     1.5  MASTERLOG=$LOGPREFIX/isatest.log
     1.6  
     1.7 +TMP=/tmp/isatest-makeall.$$
     1.8 +
     1.9 +MAIL=~/bin/pmail
    1.10 +
    1.11  ## diagnostics
    1.12  
    1.13  PRG="$(basename "$0")"
    1.14 @@ -47,6 +51,8 @@
    1.15  
    1.16  [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    1.17  
    1.18 +LOGS=""
    1.19 +
    1.20  for SETTINGS in $@; do
    1.21  
    1.22      [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    1.23 @@ -62,29 +68,18 @@
    1.24  
    1.25      echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
    1.26  
    1.27 -    cp $DISTPREFIX/Isabelle/etc/settings $DISTPREFIX/Isabelle/etc/settings.save-$SHORT
    1.28      cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    1.29 -    $DISTPREFIX/Isabelle/bin/isatool makeall all >> $TESTLOG 2>&1 
    1.30 +    nice $DISTPREFIX/Isabelle/bin/isatool makeall -j 2 all >> $TESTLOG 2>&1 
    1.31  
    1.32      if [ $? -eq 0 ]
    1.33      then
    1.34          echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    1.35 -        mv $DISTPREFIX/Isabelle/etc/settings.save-$SHORT $DISTPREFIX/Isabelle/etc/settings
    1.36          gzip -f $TESTLOG
    1.37  	rm -rf ~/isabelle-$SHORT
    1.38      else
    1.39          echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    1.40  	FAIL="$FAIL$SHORT "
    1.41 -	for R in $MAILTO; do
    1.42 -    		mail -t $R <<EOM
    1.43 -Subject: isabelle test failed
    1.44 -
    1.45 -Test for platform $SHORT failed. Log file available at
    1.46 -
    1.47 -$HOSTNAME:$TESTLOG
    1.48 -EOM
    1.49 -	done
    1.50 -        # more action here
    1.51 +	LOGS="${LOGS}$HOSTNAME:$TESTLOG\n"
    1.52      fi
    1.53  
    1.54  done
    1.55 @@ -93,6 +88,16 @@
    1.56  
    1.57  if [ "$FAIL" != "" ]; then
    1.58  	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    1.59 +	
    1.60 +	echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
    1.61 +	echo "$LOGS" >> $TMP
    1.62 +
    1.63 +        for R in $MAILTO; do
    1.64 +	    $MAIL "isabelle test failed" $R $TMP
    1.65 +	done
    1.66 +
    1.67 +	rm $TMP
    1.68 +
    1.69  	exit 1
    1.70  else
    1.71          echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/pmail	Tue Jul 09 11:46:36 2002 +0200
     2.3 @@ -0,0 +1,56 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Gerwin Klein, TU Muenchen
     2.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.9 +#
    2.10 +# DESCRIPTION: send email platform independently.
    2.11 +
    2.12 +PRG="$(basename "$0")"
    2.13 +
    2.14 +function usage()
    2.15 +{
    2.16 +  echo
    2.17 +  echo "Usage: $PRG subject recipient body"
    2.18 +  echo
    2.19 +  echo "  Send email platform independently. Body is a file."
    2.20 +  echo
    2.21 +  exit 1
    2.22 +}
    2.23 +
    2.24 +function fail()
    2.25 +{
    2.26 +  echo "$1" >&2
    2.27 +  exit 2
    2.28 +}
    2.29 +
    2.30 +## main
    2.31 +
    2.32 +# argument checking
    2.33 +
    2.34 +[ "$1" = "-?" ] && usage
    2.35 +[ "$#" != "3" ] && usage
    2.36 +
    2.37 +SUBJECT=$1
    2.38 +TO=$2
    2.39 +BODY=$3
    2.40 +
    2.41 +[ -r $BODY ] || fail "could not read $BODY"
    2.42 +
    2.43 +case `uname` in
    2.44 +    Linux*)
    2.45 +    mail -s "$SUBJECT" $TO <$BODY
    2.46 +    ;;
    2.47 +
    2.48 +    SunOS*)
    2.49 +    mail -t $TO <<EOF
    2.50 +Subject: $SUBJECT
    2.51 +
    2.52 +`cat $BODY`
    2.53 +EOF
    2.54 +    ;;
    2.55 +
    2.56 +    *)  
    2.57 +    fail "unkown platform"
    2.58 +    ;;
    2.59 +esac