src/Pure/ROOT.ML
changeset 71086 aedd11603fb4
parent 70907 7e3f25a0cee4
child 71088 4b45d592ce29
--- 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";