Admin/isatest-check
changeset 16362 f321def7279c
parent 16178 754efc5afd5d
child 16507 ee552def8721
equal deleted inserted replaced
16361:cb31cb768a6c 16362:f321def7279c
    66     echo "Have a nice day," >> $TMP
    66     echo "Have a nice day," >> $TMP
    67     echo "  isatest" >> $TMP
    67     echo "  isatest" >> $TMP
    68 
    68 
    69     for R in $MAILTO; do
    69     for R in $MAILTO; do
    70         LOGS=$ERRORDIR/isatest*.log
    70         LOGS=$ERRORDIR/isatest*.log
    71         $MAIL "isabelle test taking to long" $R $TMP $LOGS
    71         $MAIL "isabelle test taking too long" $R $TMP $LOGS
    72     done
    72     done
    73     
    73     
    74     exit 1
    74     exit 1
    75 fi
    75 fi
    76 
    76