src/Tools/jEdit/patches/laf_fonts
author Fabian Huch <huch@in.tum.de>
Mon, 13 Nov 2023 17:25:26 +0100
changeset 78973 d91e131840a0
parent 73223 ee2e803fcf57
child 81297 07f64697408e
permissions -rw-r--r--
timing heuristic: parallelize more aggressively to utilize hosts fully;

--- 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