author | wenzelm |
Fri, 28 Jun 2024 13:14:15 +0200 | |
changeset 80442 | 7b70c5bb2807 |
parent 80441 | c420429fdf4c |
child 80443 | ab0dd21dd0ca |
--- a/src/Pure/General/utf8.scala Fri Jun 28 11:37:13 2024 +0200 +++ b/src/Pure/General/utf8.scala Fri Jun 28 13:14:15 2024 +0200 @@ -20,12 +20,12 @@ def relevant(s: CharSequence): Boolean = { var i = 0 val n = s.length - var utf8 = false - while (i < n && !utf8) { - if (s.charAt(i) >= 128) { utf8 = true } + var found = false + while (i < n && !found) { + if (s.charAt(i) >= 128) { found = true } i += 1 } - utf8 + found }