Admin/isatest-makeall
changeset 14279 00eb40463c27
parent 14035 c46ce87960fb
child 14280 d7c3691008f9
equal deleted inserted replaced
14278:ae499452700a 14279:00eb40463c27
   107     touch $RUNNING/$SHORT.running
   107     touch $RUNNING/$SHORT.running
   108 
   108 
   109     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   109     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   110 
   110 
   111     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   111     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
       
   112     cd $DISTPREFIX/Isabelle/src/Pure
       
   113     $DISTPREFIX/Isabelle/bin/isatool make Pure $MFLAGS all >> $TESTLOG 2>&1
       
   114     cd -
   112     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   115     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   113 
   116 
   114     if [ $? -eq 0 ]
   117     if [ $? -eq 0 ]
   115     then
   118     then
   116         # test log and cleanup
   119         # test log and cleanup