# HG changeset patch
# User wenzelm
# Date 1543676104 -3600
# Node ID d70767e508d71f76544b512d1d8d9e297888a0e6
# Parent  4c9b4e2c54600d9c5153c91003c3f0b92c952324
proper menu accelerator font for Java 11 (no update of jedit-build component yet);

diff -r 4c9b4e2c5460 -r d70767e508d7 src/Tools/jEdit/patches/accelerator_font
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/accelerator_font	Sat Dec 01 15:55:04 2018 +0100
@@ -0,0 +1,12 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2018-12-01 15:51:30.320182833 +0100
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2018-12-01 15:51:49.028286932 +0100
+@@ -1172,7 +1172,7 @@
+ 				return new Font("Monospaced", Font.PLAIN, 12);
+ 			}
+ 			else {
+-				Font font2 = new Font("Lucida Sans Typewriter", Font.PLAIN, font1.getSize());
++				Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
+ 				FontRenderContext frc = new FontRenderContext(null, true, false);
+ 				float scale =
+ 					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();