# HG changeset patch
# User wenzelm
# Date 1397726010 -7200
# Node ID eb088da48f868927bb0067ed0f8432f15a6f95a7
# Parent  5780bddbe9a1f483de39fa82ebfdc7fa8c1adb46
proper tooltip_lines for multi-line text;

diff -r 5780bddbe9a1 -r eb088da48f86 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Thu Apr 17 10:58:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Thu Apr 17 11:13:30 2014 +0200
@@ -49,7 +49,7 @@
       def load = button.setSelectedColor(Color_Value(string(opt_name)))
       def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
     }
-    component.tooltip = opt.print_default
+    component.tooltip = GUI.tooltip_lines(List(opt.print_default))
     component
   }
 
@@ -96,7 +96,7 @@
         text_area
       }
     component.load()
-    component.tooltip = opt.print_default
+    component.tooltip = GUI.tooltip_lines(List(opt.print_default))
     component
   }
 
diff -r 5780bddbe9a1 -r eb088da48f86 src/Tools/jEdit/src/spell_checker.scala
--- 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
   }