author | wenzelm |
Mon, 21 Sep 2015 20:45:57 +0200 | |
changeset 61220 | 1bb5a10b8ce0 |
parent 61219 | f9aaca00be49 |
child 61221 | bf194f7c4c8e |
--- 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("<html><b>Update</b></html>") { tooltip = "Update display according to the command at cursor position" reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) } }