clarified signature;
authorwenzelm
Wed, 03 Jul 2024 20:18:36 +0200
changeset 80491 b439582efc8a
parent 80490 dd2f5fb363a5
child 80492 43323d886ea3
clarified signature;
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) }