src/Pure/ROOT.ML
changeset 73834 364bac6691de
parent 73761 ef1a18e20ace
child 73835 5dae03d50db1
--- a/src/Pure/ROOT.ML	Mon Jun 07 15:13:34 2021 +0200
+++ b/src/Pure/ROOT.ML	Mon Jun 07 16:40:26 2021 +0200
@@ -27,7 +27,6 @@
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
-ML_file "ML/ml_profiling.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
@@ -47,6 +46,7 @@
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
+ML_file "ML/ml_profiling.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";