reset options last -- other parts of the system may still need them;
authorwenzelm
Mon, 20 May 2013 13:38:48 +0200
changeset 52080 02749038168b
parent 52079 291bb1f4af29
child 52081 29566b6810f7
reset options last -- other parts of the system may still need them;
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;