changeset 69448 | 51e696887b81 |
parent 69441 | 0bd51c6aaa8b |
child 69449 | b516fdf8005c |
--- a/src/Pure/ROOT.ML Mon Dec 10 23:36:29 2018 +0100 +++ b/src/Pure/ROOT.ML Tue Dec 11 19:25:35 2018 +0100 @@ -83,12 +83,12 @@ ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; -ML_file "General/bytes.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; +ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/document_id.ML";