# HG changeset patch
# User wenzelm
# Date 1274439584 -7200
# Node ID 35d45feccbc6f31692ba057a1ae1bb4cde25a11b
# Parent  49559c4e85f99916c42701b846e9f0bc29639e62
added some tooltips;

diff -r 49559c4e85f9 -r 35d45feccbc6 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:51:03 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 12:59:44 2010 +0200
@@ -63,12 +63,15 @@
     }
 
   private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
+  zoom.tooltip = "Zoom factor for basic font size"
 
   private val update = new Button("Update") {
     reactions += { case ButtonClicked(_) => handle_update() }
   }
+  update.tooltip = "Update display according to state of command at caret position"
 
   private val follow = new CheckBox("Follow")
+  follow.tooltip = "Indicate automatic update according to caret movement or state changes"
   follow.selected = true