# HG changeset patch
# User wenzelm
# Date 1739109263 -3600
# Node ID 1eda03781f76132a1ddff690dfaebfc5acff7394
# Parent  c30b6eff8fa1ae04b8948170e77e144c9ef88de3
tuned: fewer warnings in IntelliJ IDEA;

diff -r c30b6eff8fa1 -r 1eda03781f76 src/Pure/General/word.scala
--- 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))