changeset 56611 | eb088da48f86 |
parent 56603 | 4f45570e532d |
child 56622 | 891d1b8b64fb |
--- a/src/Tools/jEdit/src/spell_checker.scala Thu Apr 17 10:58:10 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Thu Apr 17 11:13:30 2014 +0200 @@ -126,7 +126,7 @@ } component.load() - component.tooltip = opt.print_default + component.tooltip = GUI.tooltip_lines(List(opt.print_default)) component }