# HG changeset patch # User wenzelm # Date 1442861157 -7200 # Node ID 1bb5a10b8ce029e20431263ef67a4d1c1bd69451 # Parent f9aaca00be49986f2f955fb54dad0b620aff32c5 tuned GUI; diff -r f9aaca00be49 -r 1bb5a10b8ce0 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 20:31:43 2015 +0200 +++ b/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 20:45:57 2015 +0200 @@ -74,7 +74,7 @@ /* controls */ - private val update_button = new Button("Update") { + private val update_button = new Button("Update") { tooltip = "Update display according to the command at cursor position" reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) } }