src/Pure/System/web_app.scala
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