# HG changeset patch # User kleing # Date 1053268220 -7200 # Node ID bb70604a07c4dcfdc9594d6078d270add7ef052d # Parent afeaca7d943aeb55f1ac28c8c334f844d908686e fix typo diff -r afeaca7d943a -r bb70604a07c4 Admin/isatest-check --- a/Admin/isatest-check Sun May 18 16:29:18 2003 +0200 +++ b/Admin/isatest-check Sun May 18 16:30:20 2003 +0200 @@ -95,7 +95,7 @@ for R in $MAILTO; do LOGS=$ERRORDIR/isatest*.log - $MAIL "isabelle test failed" $R $TMP *.log + $MAIL "isabelle test failed" $R $TMP $LOGS done rm $TMP