author | wenzelm |
Thu, 30 Jun 2022 22:49:47 +0200 | |
changeset 75640 | 3b5a2e01b73b |
parent 75639 | b8bd01897578 |
child 75641 | a7e0129b8b2d |
--- a/src/Pure/General/bytes.ML Wed Jun 29 22:33:08 2022 +0200 +++ b/src/Pure/General/bytes.ML Thu Jun 30 22:49:47 2022 +0200 @@ -48,7 +48,7 @@ (* primitive operations *) -val chunk_size = 1024 * 1024; +val chunk_size = 1024 * 1024 - 8; abstype T = Bytes of {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}