src/Tools/jEdit/src/symbols_dockable.scala
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)
 }