changeset 78614 | 4da5cdaa4dcd |
parent 77509 | 3bc49507bae5 |
child 80480 | 972f7a4cdc0e |
--- a/src/Tools/jEdit/src/document_dockable.scala Tue Aug 29 18:13:30 2023 +0200 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Aug 29 18:17:04 2023 +0200 @@ -278,7 +278,7 @@ private val auto_build_button = new JEdit_Options.Bool_GUI(document_auto, "Auto") { - tooltip = Word.capitalize(document_auto.description) + tooltip = Word.capitalized(document_auto.description) override def clicked(state: Boolean): Unit = { super.clicked(state)