# HG changeset patch
# User wenzelm
# Date 1583528488 -3600
# Node ID 95a4db22b70f9d8140ed6badd8a2f9a6c08e8fbc
# Parent  e977609c30eb6502c1422895281d6dbb70cc29b8
tuned;

diff -r e977609c30eb -r 95a4db22b70f src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Fri Mar 06 20:33:16 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Mar 06 22:01:28 2020 +0100
@@ -231,7 +231,7 @@
 isabelle.increase-font-size.shortcut=C+PLUS
 isabelle.increase-font-size2.label=Increase font size (clone)
 isabelle.increase-font-size2.shortcut=C+EQUALS
-isabelle.jconsole.label=Java/VM Monitor
+isabelle.jconsole.label=Java/VM monitor
 isabelle.last-error.label=Go to last error
 isabelle.last-error.shortcut=CS+z
 isabelle.message.label=Show message