src/Pure/General/utf8.scala
changeset 80494 d1240adc30ce
parent 80492 43323d886ea3
child 80508 8585399f26f6
--- a/src/Pure/General/utf8.scala	Wed Jul 03 20:59:30 2024 +0200
+++ b/src/Pure/General/utf8.scala	Wed Jul 03 21:11:53 2024 +0200
@@ -50,7 +50,7 @@
       }
     }
     for (i <- 0L until size) {
-      val c: Char = bytes(i)
+      val c = bytes.char(i)
       if (c < 128) { flush(); buf.append(c) }
       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)