--- 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) }