Admin/isatest-makeall
author kleing
Thu Jun 20 22:17:28 2002 +0200 (2002-06-20)
changeset 13233 5ab7bac534c9
parent 13232 8b1b5e8c4bd6
child 13236 568bc754d303
permissions -rwxr-xr-x
tuned
kleing@13231
     1
#!/usr/bin/env bash
kleing@13231
     2
#
kleing@13231
     3
# $Id$
kleing@13231
     4
# Author: Gerwin Klein, TU Muenchen
kleing@13231
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
kleing@13231
     6
#
kleing@13231
     7
# DESCRIPTION: Run isatool makeall from specified distribution and settings.
kleing@13231
     8
#              Send email if it fails.
kleing@13231
     9
kleing@13231
    10
## global settings
kleing@13232
    11
LOGPREFIX=~/log
kleing@13231
    12
kleing@13231
    13
## diagnostics
kleing@13231
    14
kleing@13231
    15
PRG="$(basename "$0")"
kleing@13231
    16
kleing@13231
    17
function usage()
kleing@13231
    18
{
kleing@13231
    19
  echo
kleing@13231
    20
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
kleing@13231
    21
  echo
kleing@13231
    22
  echo "  Run isatool makeall from specified distribution and settings."
kleing@13231
    23
  echo "  Send email if it fails."
kleing@13231
    24
  echo
kleing@13231
    25
  exit 1
kleing@13231
    26
}
kleing@13231
    27
kleing@13231
    28
function fail()
kleing@13231
    29
{
kleing@13231
    30
  echo "$1" >&2
kleing@13231
    31
  exit 2
kleing@13231
    32
}
kleing@13231
    33
kleing@13231
    34
## main
kleing@13231
    35
kleing@13231
    36
# argument checking
kleing@13231
    37
kleing@13231
    38
[ "$1" = "-?" ] && usage
kleing@13231
    39
[ "$#" -lt "2" ] && usage
kleing@13231
    40
kleing@13231
    41
DISTPREFIX=$1
kleing@13231
    42
shift
kleing@13231
    43
kleing@13231
    44
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
kleing@13231
    45
kleing@13231
    46
for SETTINGS in $@; do
kleing@13231
    47
kleing@13231
    48
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
kleing@13231
    49
    
kleing@13231
    50
kleing@13231
    51
    # logfile setup
kleing@13231
    52
kleing@13231
    53
    DATE=$(date "+%d-%b-%Y")
kleing@13231
    54
    SHORT=${SETTINGS##*/}
kleing@13231
    55
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
kleing@13231
    56
kleing@13231
    57
    # the test
kleing@13231
    58
kleing@13231
    59
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
kleing@13231
    60
kleing@13233
    61
    cp $DISTPREFIX/Isabelle/etc/settings $DISTPREFIX/Isabelle/etc/settings.save-$SHORT
kleing@13233
    62
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
kleing@13231
    63
    $DISTPREFIX/Isabelle/bin/isatool makeall all >> $TESTLOG 2>&1 
kleing@13231
    64
kleing@13231
    65
    if [ $? -eq 0 ]
kleing@13231
    66
    then
kleing@13231
    67
        echo ------------------- test successfull --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13233
    68
        mv $DISTPREFIX/Isabelle/etc/settings-$SHORT $DISTPREFIX/Isabelle/etc/settings
kleing@13231
    69
        gzip -f $TESTLOG
kleing@13231
    70
    else
kleing@13231
    71
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13231
    72
        # more action here
kleing@13231
    73
        exit 1
kleing@13231
    74
    fi
kleing@13231
    75
kleing@13231
    76
done
kleing@13231
    77
kleing@13231
    78
# end