src/Pure/ROOT.ML
changeset 75615 4494cd69f97f
parent 75567 94321fd25c8a
child 75620 44815dc2b8f9
--- a/src/Pure/ROOT.ML	Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/ROOT.ML	Fri Jun 24 23:31:28 2022 +0200
@@ -78,8 +78,9 @@
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash.ML";
+ML_file "General/file_stream.ML";
+ML_file "General/bytes.ML";
 ML_file "General/file.ML";
-ML_file "General/bytes.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";