# HG changeset patch
# User wenzelm
# Date 1573225869 -3600
# Node ID aedd11603fb4b960043cdaef96018faea19978bf
# Parent  950e1cfe0fe46e4c5c69311df46db2eeed1fcd55
tuned modules;

diff -r 950e1cfe0fe4 -r aedd11603fb4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Nov 08 12:07:39 2019 +0100
+++ b/src/Pure/ROOT.ML	Fri Nov 08 16:11:09 2019 +0100
@@ -111,6 +111,7 @@
 subsection "Concurrency within the ML runtime";
 
 ML_file "ML/exn_properties.ML";
+ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "ML/ml_statistics.ML";
 
@@ -199,7 +200,6 @@
 ML_file "ML/ml_env.ML";
 ML_file "ML/ml_options.ML";
 ML_file "ML/ml_print_depth.ML";
-ML_file_no_debug "ML/exn_debugger.ML";
 ML_file_no_debug "Isar/runtime.ML";
 ML_file "PIDE/execution.ML";
 ML_file "ML/ml_compiler.ML";