Admin/isatest-check
changeset 14039 bb70604a07c4
parent 14038 afeaca7d943a
child 14170 edd5a2ea3807
equal deleted inserted replaced
14038:afeaca7d943a 14039:bb70604a07c4
    93     echo "Have a nice day," >> $TMP
    93     echo "Have a nice day," >> $TMP
    94     echo "  isatest" >> $TMP
    94     echo "  isatest" >> $TMP
    95 
    95 
    96     for R in $MAILTO; do
    96     for R in $MAILTO; do
    97         LOGS=$ERRORDIR/isatest*.log
    97         LOGS=$ERRORDIR/isatest*.log
    98         $MAIL "isabelle test failed" $R $TMP *.log
    98         $MAIL "isabelle test failed" $R $TMP $LOGS
    99     done
    99     done
   100 
   100 
   101     rm $TMP
   101     rm $TMP
   102     exit 1
   102     exit 1
   103 fi
   103 fi