author | wenzelm |
Thu, 29 Jun 2017 11:58:00 +0200 | |
changeset 66213 | 9380ec9babfb |
parent 66212 | f41396c15bb1 |
child 66214 | eec1c99e1bdc |
--- a/src/Tools/VSCode/src/state_panel.scala Thu Jun 29 11:42:42 2017 +0200 +++ b/src/Tools/VSCode/src/state_panel.scala Thu Jun 29 11:58:00 2017 +0200 @@ -135,7 +135,7 @@ tooltip = "Locate printed command within source text", script = "invoke_locate()") - private val controls: XML.Elem = + private def controls: XML.Elem = HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button))