minor performance tuning;

--- a/src/Pure/General/bytes.scala	Sun Jun 16 11:55:25 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jun 16 11:59:16 2024 +0200
@@ -188,9 +188,11 @@
       if (n > 0) {
         if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) }
         else {
-          for (i <- 0 until n) {
+          var i = 0
+          while (i < n) {
+            buffer.write(s.charAt(i).toByte)
             size += 1
-            buffer.write(s.charAt(i).toByte)
+            i += 1
             buffer_check()
           }
         }