| changeset 75592 | f72b88f2842c |
| parent 75581 | 29654a8e9374 |
| child 75594 | 303f885d4a8c |
--- a/src/Pure/General/bytes.ML Wed Jun 22 14:22:08 2022 +0200 +++ b/src/Pure/General/bytes.ML Wed Jun 22 14:26:11 2022 +0200 @@ -138,6 +138,9 @@ val buffer = build o fold add o Buffer.contents; + +(* IO *) + fun read_block limit = File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));