# HG changeset patch
# User wenzelm
# Date 1665578945 -7200
# Node ID f0d8f659b19a2a3402017daaace2876db35831b0
# Parent  13b733e78c269ebcce093522441756d1192d8d5e
less ambitious Bytes.chunk_size, which is presumably more stable with memory management under heavy load;

diff -r 13b733e78c26 -r f0d8f659b19a src/Pure/General/bytes.ML
--- 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*)}