author | wenzelm |
Sun, 09 Feb 2025 14:54:23 +0100 | |
changeset 82124 | 1eda03781f76 |
parent 82123 | c30b6eff8fa1 |
child 82125 | f6460ae54866 |
--- a/src/Pure/General/word.scala Sun Feb 09 13:11:20 2025 +0100 +++ b/src/Pure/General/word.scala Sun Feb 09 14:54:23 2025 +0100 @@ -26,7 +26,7 @@ def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) def capitalized(str: String): String = - if (str.length == 0) str + if (str.isEmpty) str else { val n = Character.charCount(str.codePointAt(0)) uppercase(str.substring(0, n)) + lowercase(str.substring(n))