--- a/Admin/components/components.sha1 Tue Dec 22 23:59:45 2020 +0100
+++ b/Admin/components/components.sha1 Wed Dec 23 15:01:50 2020 +0100
@@ -183,6 +183,7 @@
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz
533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
+f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Tue Dec 22 23:59:45 2020 +0100
+++ b/Admin/components/main Wed Dec 23 15:01:50 2020 +0100
@@ -6,7 +6,7 @@
e-2.5-1
isabelle_fonts-20190717
jdk-11.0.9+11
-jedit_build-20200908
+jedit_build-20201223
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/panel_font Wed Dec 23 15:01:50 2020 +0100
@@ -0,0 +1,28 @@
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-09-03 05:31:02.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-12-23 13:16:31.059779643 +0100
+@@ -52,6 +52,7 @@
+ import javax.swing.JComponent;
+ import javax.swing.JPanel;
+ import javax.swing.JPopupMenu;
++import javax.swing.JMenuItem;
+ import javax.swing.JToggleButton;
+ import javax.swing.UIManager;
+ import javax.swing.border.Border;
+@@ -163,6 +164,7 @@
+ {
+ button = new JToggleButton();
+ button.setMargin(new Insets(1,1,1,1));
++ button.setFont(new JMenuItem().getFont());
+ }
+ GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
+ button.setRequestFocusEnabled(false);
+@@ -690,8 +692,6 @@
+ renderHints = new RenderingHints(
+ RenderingHints.KEY_ANTIALIASING,
+ RenderingHints.VALUE_ANTIALIAS_ON);
+- renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
+- RenderingHints.VALUE_FRACTIONALMETRICS_ON);
+ renderHints.put(RenderingHints.KEY_RENDERING,
+ RenderingHints.VALUE_RENDER_QUALITY);
+ } //}}}