Admin/isatest-check
changeset 14038 afeaca7d943a
parent 14035 c46ce87960fb
child 14039 bb70604a07c4
equal deleted inserted replaced
14037:3b7f3eec9684 14038:afeaca7d943a
     8 #              generates development snapshot if test ok
     8 #              generates development snapshot if test ok
     9 
     9 
    10 # source bashrc, we're called by cron
    10 # source bashrc, we're called by cron
    11 . ~/.bashrc
    11 . ~/.bashrc
    12 
    12 
       
    13 # produce empty list for patterns like isatest-*.log if no 
       
    14 # such file exists 
       
    15 shopt -s nullglob
    13 
    16 
    14 ## global settings
    17 ## global settings
    15 
    18 
    16 # send mail to:
    19 # send mail to:
    17 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    20 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    88 if [ -e $ERRORLOG ]; then
    91 if [ -e $ERRORLOG ]; then
    89     cat $ERRORLOG > $TMP
    92     cat $ERRORLOG > $TMP
    90     echo "Have a nice day," >> $TMP
    93     echo "Have a nice day," >> $TMP
    91     echo "  isatest" >> $TMP
    94     echo "  isatest" >> $TMP
    92 
    95 
    93     cd $ERRORDIR
       
    94     for R in $MAILTO; do
    96     for R in $MAILTO; do
       
    97         LOGS=$ERRORDIR/isatest*.log
    95         $MAIL "isabelle test failed" $R $TMP *.log
    98         $MAIL "isabelle test failed" $R $TMP *.log
    96     done
    99     done
    97 
   100 
    98     rm $TMP
   101     rm $TMP
    99     exit 1
   102     exit 1