# HG changeset patch
# User wenzelm
# Date 1612199564 -3600
# Node ID ee2e803fcf5756026b0bd33bf0e2ba0a7fbd1f3b
# Parent  e18191f2aed9281c7f8db65133f950b393caee75
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);

diff -r e18191f2aed9 -r ee2e803fcf57 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Feb 01 17:15:00 2021 +0100
+++ b/Admin/components/components.sha1	Mon Feb 01 18:12:44 2021 +0100
@@ -192,6 +192,7 @@
 1c753beb93e92e95e99e8ead23a68346bd1af44a  jedit_build-20200610.tar.gz
 533b1ee6459f59bcbe4f09e214ad2cb990fb6952  jedit_build-20200908.tar.gz
 f9966b5ed26740bb5b8bddbfe947fcefaea43d4d  jedit_build-20201223.tar.gz
+0bdbd36eda5992396e9c6b66aa24259d4dd7559c  jedit_build-20210201.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
diff -r e18191f2aed9 -r ee2e803fcf57 Admin/components/main
--- a/Admin/components/main	Mon Feb 01 17:15:00 2021 +0100
+++ b/Admin/components/main	Mon Feb 01 18:12:44 2021 +0100
@@ -7,7 +7,7 @@
 flatlaf-1.0-rc2
 isabelle_fonts-20190717
 jdk-15.0.2+7
-jedit_build-20201223
+jedit_build-20210201
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6
diff -r e18191f2aed9 -r ee2e803fcf57 src/Tools/jEdit/patches/laf_fonts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/laf_fonts	Mon Feb 01 18:12:44 2021 +0100
@@ -0,0 +1,13 @@
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2021-02-01 18:00:07.541681144 +0100
+@@ -414,7 +414,9 @@
+ 
+ 		// adjust swing properties for button, menu, and label, and list and
+ 		// textfield fonts
+-		setFonts();
++		if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
++			setFonts();
++		}
+ 
+ 		// This is handled a little differently from other jEdit settings
+ 		// as this flag needs to be known very early in the