minor performance tuning;

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