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";