diff -r 52f71e3816d8 -r 5e8dca75c699 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Jun 16 14:19:51 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jun 16 14:21:57 2024 +0200
@@ -23,8 +23,8 @@
   /* internal sizes */
 
   private val array_size: Long = Int.MaxValue - 8  // see java.io.InputStream.MAX_BUFFER_SIZE
+  private val block_size: Int = 16384  // see java.io.InputStream.DEFAULT_BUFFER_SIZE
   private val chunk_size: Long = Space.MiB(100).bytes
-  private val block_size: Int = 8192
 
   private def make_size(chunks: Array[Array[Byte]], buffer: Array[Byte]): Long =
     chunks.foldLeft(buffer.length.toLong)((n, chunk) => n + chunk.length)