# HG changeset patch
# User kleing
# Date 1070681548 -3600
# Node ID d7c3691008f9f2671a0ed03d759738638392842c
# Parent  00eb40463c27ed3fbc95e2f7689014a3e676ab0d
revert to 1.18, changed Distribution/lib/Tools/makeall instead

diff -r 00eb40463c27 -r d7c3691008f9 Admin/isatest-makeall
--- 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 ]