diff -r c92356464bb3 -r 5fe811816fa3 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Thu Jun 27 00:09:37 2024 +0200 +++ b/src/Pure/General/bytes.scala Thu Jun 27 00:11:53 2024 +0200 @@ -217,14 +217,6 @@ buffer_check() } - def += (s: CharSequence): Unit = { - val n = s.length - if (n > 0) { - if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) } - else { for (i <- 0 until n) { this += s.charAt(i).toByte } } - } - } - def += (array: Array[Byte], offset: Int, length: Int): Unit = { if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) { throw new IndexOutOfBoundsException @@ -244,6 +236,9 @@ } } + def += (s: CharSequence): Unit = + if (s.length > 0) { this += UTF8.bytes(s.toString) } + def += (array: Array[Byte]): Unit = { this += (array, 0, array.length) } def += (a: Subarray): Unit = { this += (a.array, a.offset, a.length) }