src/Pure/ROOT.ML
changeset 82092 93195437fdee
parent 82064 878a67422fb4
child 82143 a43e39c52f26
--- a/src/Pure/ROOT.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/ROOT.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -54,6 +54,7 @@
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
+ML_file "General/time.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
@@ -94,7 +95,6 @@
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
-ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";