--- a/src/Tools/jEdit/src/jEdit.props Thu Mar 12 20:58:18 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Thu Mar 12 21:02:05 2020 +0100
@@ -185,6 +185,7 @@
foldPainter=Circle
gatchan.highlight.overview=false
helpviewer.font=Isabelle DejaVu Serif
+helpviewer.fontsize=12
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=
@@ -269,7 +270,9 @@
lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
match-bracket.shortcut2=C+9
metal.primary.font=Isabelle DejaVu Sans
+metal.primary.fontsize=12
metal.secondary.font=Isabelle DejaVu Sans
+metal.secondary.fontsize=12
navigator.showOnToolbar=true
next-bracket.shortcut2=C+e C+9
new-file-in-mode.shortcut=