src/Pure/ROOT.ML
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";