changeset 73558 | a5d1d1e2f109 |
parent 73523 | 2cd23d587db9 |
child 73587 | d1767bcb79ec |
--- a/src/Pure/ROOT.ML Sun Apr 11 21:23:51 2021 +0200 +++ b/src/Pure/ROOT.ML Sun Apr 11 21:32:09 2021 +0200 @@ -88,8 +88,8 @@ ML_file "General/timing.ML"; ML_file "General/sha1.ML"; +ML_file "PIDE/yxml.ML"; ML_file "PIDE/byte_message.ML"; -ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML";