changeset 80444 | 2bbcfcfca0cd |
parent 80443 | ab0dd21dd0ca |
child 80445 | 00f5e829d8b4 |
--- a/src/Pure/General/symbol.scala Fri Jun 28 13:20:18 2024 +0200 +++ b/src/Pure/General/symbol.scala Fri Jun 28 13:46:06 2024 +0200 @@ -541,8 +541,7 @@ if (encode(decoded) == text) decoded else { val bad = new mutable.ListBuffer[Symbol] - for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) - bad += s + for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) bad += s error("Bad Unicode symbols in text: " + commas_quote(bad)) } }