| changeset 80494 | d1240adc30ce |
| parent 80396 | 94875d8cc8bd |
| child 80648 | 572b096c889a |
--- a/src/Pure/System/web_app.scala Wed Jul 03 20:59:30 2024 +0200 +++ b/src/Pure/System/web_app.scala Wed Jul 03 21:11:53 2024 +0200 @@ -125,7 +125,7 @@ var sep_ok = true var sep_i = 0 while (sep_ok && sep_i < sep.length) { - if (bytes(bytes_i + sep_i) == sep(sep_i)) { + if (bytes.char(bytes_i + sep_i) == sep(sep_i)) { sep_i += 1 } else { bytes_i += 1