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