even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);
--- a/src/Pure/System/session.ML Mon May 20 14:04:21 2013 +0200
+++ b/src/Pure/System/session.ML Mon May 20 15:42:14 2013 +0200
@@ -56,7 +56,6 @@
Outer_Syntax.check_syntax ();
Future.shutdown ();
Event_Timer.shutdown ();
- Options.reset_default ();
session_finished := true);
end;
--- a/src/Pure/build Mon May 20 14:04:21 2013 +0200
+++ b/src/Pure/build Mon May 20 15:42:14 2013 +0200
@@ -80,6 +80,7 @@
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
-e "Command_Line.tool0 Session.finish;" \
+ -e "Options.reset_default ();" \
-q -w RAW_ML_SYSTEM "$OUTPUT"
fi
fi