author | kleing |
Sat, 06 Dec 2003 04:32:28 +0100 | |
changeset 14280 | d7c3691008f9 |
parent 14279 | 00eb40463c27 |
child 14281 | a8c4a1e63071 |
--- a/Admin/isatest-makeall Sat Dec 06 04:29:30 2003 +0100 +++ b/Admin/isatest-makeall Sat Dec 06 04:32:28 2003 +0100 @@ -109,9 +109,6 @@ echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings - cd $DISTPREFIX/Isabelle/src/Pure - $DISTPREFIX/Isabelle/bin/isatool make Pure $MFLAGS all >> $TESTLOG 2>&1 - cd - $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 if [ $? -eq 0 ]