Admin/isatest/isatest-makeall
changeset 41967 6aa69999da8f
parent 39686 8b9f971ace20
child 44978 a04f3eb3943c
equal deleted inserted replaced
41966:d65835c381dd 41967:6aa69999da8f
   151     if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
   151     if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
   152         echo "--- cleaning up old $ISABELLE_HOME_USER"
   152         echo "--- cleaning up old $ISABELLE_HOME_USER"
   153         rm -rf $ISABELLE_HOME_USER
   153         rm -rf $ISABELLE_HOME_USER
   154     fi
   154     fi
   155 
   155 
       
   156     cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
   156     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   157     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   157     (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)
   158     (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)
   158 
   159 
   159     if [ $? -eq 0 ]
   160     if [ $? -eq 0 ]
   160     then
   161     then