equal
deleted
inserted
replaced
1 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java |
1 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java |
2 --- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2018-12-01 15:51:30.320182833 +0100 |
2 --- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2018-04-09 01:58:07.000000000 +0200 |
3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2018-12-01 15:51:49.028286932 +0100 |
3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2019-02-24 12:19:52.134389619 +0100 |
4 @@ -1172,7 +1172,7 @@ |
4 @@ -1172,7 +1172,7 @@ |
5 return new Font("Monospaced", Font.PLAIN, 12); |
5 return new Font("Monospaced", Font.PLAIN, 12); |
6 } |
6 } |
7 else { |
7 else { |
8 - Font font2 = new Font("Lucida Sans Typewriter", Font.PLAIN, font1.getSize()); |
8 - Font font2 = new Font("Lucida Sans Typewriter", Font.PLAIN, font1.getSize()); |