author | wenzelm |
Wed, 12 Oct 2022 14:49:05 +0200 | |
changeset 76277 | f0d8f659b19a |
parent 76276 | 13b733e78c26 |
child 76278 | 6aeb18e8a557 |
--- a/src/Pure/General/bytes.ML Wed Oct 12 13:01:06 2022 +0200 +++ b/src/Pure/General/bytes.ML Wed Oct 12 14:49:05 2022 +0200 @@ -48,7 +48,7 @@ (* primitive operations *) -val chunk_size = 1024 * 1024 - 8; +val chunk_size = 65000; abstype T = Bytes of {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}