# HG changeset patch
# User wenzelm
# Date 1718475293 -7200
# Node ID 8c8a2c483fc78345bce6ae793a74fdb2177a8f7d
# Parent  9db3959531061c747b7ede6d789ec4e7f9390b26
tuned;

diff -r 9db395953106 -r 8c8a2c483fc7 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 20:14:24 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 20:14:53 2024 +0200
@@ -158,9 +158,9 @@
   }
 
   final class Builder private[Bytes](chunks_size: Int, buffer_size: Int) {
-    var chunks = new ArrayBuffer[Array[Byte]](chunks_size)
-    var buffer = new ByteArrayOutputStream(buffer_size)
-    def buffer_free(): Int = chunk_size.toInt - buffer.size()
+    private var chunks = new ArrayBuffer[Array[Byte]](chunks_size)
+    private var buffer = new ByteArrayOutputStream(buffer_size)
+    private def buffer_free(): Int = chunk_size.toInt - buffer.size()
 
     def += (array: Array[Byte], offset: Int, length: Int): Unit = {
       if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {