# HG changeset patch
# User wenzelm
# Date 1369049928 -7200
# Node ID 02749038168b908c3e679d682d24bc5a5f41cac9
# Parent  291bb1f4af295e2efce7513b7308b67c083b3373
reset options last -- other parts of the system may still need them;

diff -r 291bb1f4af29 -r 02749038168b src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon May 20 13:29:45 2013 +0200
+++ b/src/Pure/System/session.ML	Mon May 20 13:38:48 2013 +0200
@@ -54,9 +54,9 @@
   Present.finish ();
   Keyword.status ();
   Outer_Syntax.check_syntax ();
-  Options.reset_default ();
   Future.shutdown ();
   Event_Timer.shutdown ();
+  Options.reset_default ();
   session_finished := true);
 
 end;