# HG changeset patch
# User wenzelm
# Date 1369057334 -7200
# Node ID f852d08376f9b0be16dc3b26eb79b8d0ce08acb5
# Parent  559e1398b70ea7a722a82b6a6c4918b64ae52390
even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);

diff -r 559e1398b70e -r f852d08376f9 src/Pure/System/session.ML
--- 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;
diff -r 559e1398b70e -r f852d08376f9 src/Pure/build
--- 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