# HG changeset patch
# User wenzelm
# Date 1439198416 -7200
# Node ID 9b26f3118e40f17d3161b4c59f080e7ecb6e5b84
# Parent  6b7d10331b6b487efd78b4a49c66d2fcf4a27106
clarified ML options;

diff -r 6b7d10331b6b -r 9b26f3118e40 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Aug 08 22:08:43 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 11:20:16 2015 +0200
@@ -152,6 +152,7 @@
     val evaluate_verbose = evaluate {SML = SML, verbose = true};
     val context1 = ML_Context.the_generic_context ()
       |> Context_Position.set_visible_generic false
+      |> Config.put_generic ML_Options.debugger false
       |> ML_Env.add_name_space {SML = SML}
           (ML_Debugger.debug_name_space (the_debug_state thread_name index));
     val context2 =