changeset 56609 | 5ac67041ccf8 |
parent 56600 | 628e039cc34d |
child 56622 | 891d1b8b64fb |
--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Apr 16 21:51:41 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Apr 17 10:54:10 2014 +0200 @@ -85,7 +85,8 @@ } reactions += { case ValueChanged(`search`) => delay_search.invoke() } }, "Search Symbols") - pages.map(p => p.title = Word.implode(Word.explode('_', p.title).map(Word.capitalize(_)))) + pages.map(p => + p.title = Word.implode(Word.explode('_', p.title).map(Word.perhaps_capitalize(_)))) } set_content(group_tabs) }