diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-10-29 11:50:54.062016616 +0100
@@ -1094,9 +1094,7 @@
return new Font("Monospaced", Font.PLAIN, 12);
}
else {
- Font font2 =
- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
- 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();