diff -r dd2f5fb363a5 -r b439582efc8a src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Wed Jul 03 15:24:34 2024 +0200 +++ b/src/Pure/General/bytes.scala Wed Jul 03 20:18:36 2024 +0200 @@ -45,7 +45,7 @@ val empty: Bytes = reuse_array(new Array(0)) - def apply(s: CharSequence): Bytes = + def apply(s: String): Bytes = if (s.isEmpty) empty else Builder.use(hint = s.length) { builder => builder += s } @@ -242,8 +242,8 @@ } } - def += (s: CharSequence): Unit = - if (s.length > 0) { builder += UTF8.bytes(s.toString) } + def += (s: String): Unit = + if (s.length > 0) { builder += UTF8.bytes(s) } def += (array: Array[Byte]): Unit = { builder += (array, 0, array.length) }