Admin/isatest-check
changeset 14035 c46ce87960fb
parent 13993 88a8911bb65d
child 14038 afeaca7d943a
equal deleted inserted replaced
14034:55ba81e3502b 14035:c46ce87960fb
    26 
    26 
    27 # mail program
    27 # mail program
    28 MAIL=$HOME/bin/pmail
    28 MAIL=$HOME/bin/pmail
    29 
    29 
    30 # where the logs are
    30 # where the logs are
    31 ERRORLOG=$HOME/var/error.log
    31 ERRORDIR=$HOME/var
       
    32 ERRORLOG=$ERRORDIR/error.log
    32 MASTERLOG=$HOME/log/isatest.log
    33 MASTERLOG=$HOME/log/isatest.log
    33 
    34 
    34 # where the test-still-running files are
    35 # where the test-still-running files are
    35 RUNNING=$HOME/var/running
    36 RUNNING=$HOME/var/running
    36 
    37 
    87 if [ -e $ERRORLOG ]; then
    88 if [ -e $ERRORLOG ]; then
    88     cat $ERRORLOG > $TMP
    89     cat $ERRORLOG > $TMP
    89     echo "Have a nice day," >> $TMP
    90     echo "Have a nice day," >> $TMP
    90     echo "  isatest" >> $TMP
    91     echo "  isatest" >> $TMP
    91 
    92 
       
    93     cd $ERRORDIR
    92     for R in $MAILTO; do
    94     for R in $MAILTO; do
    93         $MAIL "isabelle test failed" $R $TMP
    95         $MAIL "isabelle test failed" $R $TMP *.log
    94     done
    96     done
    95 
    97 
    96     rm $TMP
    98     rm $TMP
    97     exit 1
    99     exit 1
    98 fi
   100 fi