bin/isabelle
changeset 4355 68c7c544570c
parent 4333 1d326b826851
child 4516 f90b2d459a1b
equal deleted inserted replaced
4354:7f4da01bdf0e 4355:68c7c544570c
   174 if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
   174 if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
   175   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   175   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   176 else
   176 else
   177   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   177   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   178 fi
   178 fi
   179 
   179 RC=$?
   180 
   180 
   181 #Do not even think of 'rm -r'!!
   181 #Do not even think of 'rm -r'!!
   182 rmdir $ISABELLE_TMP
   182 rmdir $ISABELLE_TMP
       
   183 
       
   184 exit $RC