Admin/isatest-makeall
changeset 13962 908f6776a59b
parent 13924 09f6f2fefb25
child 13985 3852929a8d1d
equal deleted inserted replaced
13961:233dd3bb2390 13962:908f6776a59b
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     6 #
     7 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
     7 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
     8 #              Send email if it fails.
     8 #              Send email if it fails.
     9 
     9 
       
    10 # canoncical home for all platforms
       
    11 HOME=/usr/stud/isatest
       
    12 
    10 ## global settings
    13 ## global settings
    11 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    14 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    12 
    15 
    13 LOGPREFIX=~/log
    16 LOGPREFIX=$HOME/log
    14 
    17 
    15 MASTERLOG=$LOGPREFIX/isatest.log
    18 MASTERLOG=$LOGPREFIX/isatest.log
    16 
    19 
    17 TMP=/tmp/isatest-makeall.$$
    20 TMP=/tmp/isatest-makeall.$$
    18 
    21 
    19 MAIL=~/bin/pmail
    22 MAIL=$HOME/bin/pmail
    20 
    23 
    21 ## diagnostics
    24 ## diagnostics
    22 
    25 
    23 PRG="$(basename "$0")"
    26 PRG="$(basename "$0")"
    24 
    27 
   105 
   108 
   106     if [ $? -eq 0 ]
   109     if [ $? -eq 0 ]
   107     then
   110     then
   108         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   111         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   109         gzip -f $TESTLOG
   112         gzip -f $TESTLOG
   110 	rm -rf ~/isabelle-$SHORT
   113 	rm -rf $HOME/isabelle-$SHORT
   111     else
   114     else
   112         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   115         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   113 	FAIL="$FAIL$SHORT "
   116 	FAIL="$FAIL$SHORT "
   114 	LOGS="${LOGS}$TESTLOG "
   117 	LOGS="${LOGS}$TESTLOG "
   115     fi
   118     fi