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)