# HG changeset patch
# User wenzelm
# Date 1584043325 -3600
# Node ID 3cad8ffee92c21f9784425f06bd0f4f87dea7a03
# Parent  c983fd846c9c77e82d02e2555e4c9aaed607a5b2
more explicit defaults;

diff -r c983fd846c9c -r 3cad8ffee92c src/Tools/jEdit/src/jEdit.props
--- 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=