changeset 56552 | 76cf86240cb7 |
parent 55825 | 694833e3e4a0 |
child 56599 | c4424d8c890f |
--- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 12 21:00:04 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 12 21:38:38 2014 +0200 @@ -85,7 +85,7 @@ } reactions += { case ValueChanged(`search`) => delay_search.invoke() } }, "Search Symbols") - pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") ) + pages.map(p => p.title = space_explode('_', p.title).map(Library.capitalize(_)).mkString(" ")) } set_content(group_tabs) }