|
--- 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
