# HG changeset patch
# User wenzelm
# Date 1719573255 -7200
# Node ID 7b70c5bb28071a6aa8371225f6f55081bc7b7ab2
# Parent  c420429fdf4c843cb327792ff1fba9e926f64eb6
tuned;

diff -r c420429fdf4c -r 7b70c5bb2807 src/Pure/General/utf8.scala
--- 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
   }