| changeset 72976 | 51442c6dc296 |
| parent 72250 | 13976f92a2d0 |
| child 73340 | 0ffcad1f6130 |
--- a/src/Tools/jEdit/src/status_widget.scala Mon Dec 21 22:03:39 2020 +0100 +++ b/src/Tools/jEdit/src/status_widget.scala Mon Dec 21 22:47:53 2020 +0100 @@ -149,7 +149,7 @@ setToolTipText("Java heap memory (double-click for monitor application)") - override def action: String = "isabelle.jconsole" + override def action: String = "isabelle.java-monitor" } class Java_Factory extends StatusWidgetFactory