--- a/src/Pure/mk Fri Feb 05 20:57:18 1999 +0100
+++ b/src/Pure/mk Fri Feb 05 20:57:37 1999 +0100
@@ -87,6 +87,7 @@
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
+ RC=$?
else
ITEM="RAW"
echo -n "Building $ITEM ... "
@@ -96,10 +97,9 @@
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "use\"$COMPAT\" handle _ => exit 1;;" \
-q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
+ RC=$?
fi
-RC=$?
-
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)