Admin/isatest-makeall
changeset 14279 00eb40463c27
parent 14035 c46ce87960fb
child 14280 d7c3691008f9
--- a/Admin/isatest-makeall	Fri Dec 05 19:39:39 2003 +0100
+++ b/Admin/isatest-makeall	Sat Dec 06 04:29:30 2003 +0100
@@ -109,6 +109,9 @@
     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 ]