| changeset 83525 | e2e56b016194 |
| parent 83511 | 4729ac19c03c |
| child 83544 | d1a66e53c15c |
--- a/src/Pure/ROOT.ML Fri Nov 07 17:12:21 2025 +0100 +++ b/src/Pure/ROOT.ML Fri Nov 07 18:25:47 2025 +0100 @@ -98,6 +98,7 @@ ML_file "General/timing.ML"; ML_file "General/sha1.ML"; +ML_file "ML/ml_process.ML"; ML_file "ML/ml_profiling.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/protocol_message.ML";