src/Tools/jEdit/patches/accelerator_font
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 69392 d70767e508d7
permissions -rw-r--r--
formal update of patches -- no change of content;
wenzelm@69392
     1
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
wenzelm@70019
     2
--- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2018-04-09 01:58:07.000000000 +0200
wenzelm@70019
     3
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2019-02-24 12:19:52.134389619 +0100
wenzelm@69392
     4
@@ -1172,7 +1172,7 @@
wenzelm@69392
     5
 				return new Font("Monospaced", Font.PLAIN, 12);
wenzelm@69392
     6
 			}
wenzelm@69392
     7
 			else {
wenzelm@69392
     8
-				Font font2 = new Font("Lucida Sans Typewriter", Font.PLAIN, font1.getSize());
wenzelm@69392
     9
+				Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
wenzelm@69392
    10
 				FontRenderContext frc = new FontRenderContext(null, true, false);
wenzelm@69392
    11
 				float scale =
wenzelm@69392
    12
 					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();