# HG changeset patch
# User wenzelm
# Date 1747832988 -7200
# Node ID 60bd591ef3fc4be7e22c259369cc14abb6d37263
# Parent  21c3b55787a60f167f6020d6313629da50df8fc0
redundant;

diff -r 21c3b55787a6 -r 60bd591ef3fc src/Tools/jEdit/patches/laf_fonts
--- a/src/Tools/jEdit/patches/laf_fonts	Wed May 21 14:38:46 2025 +0200
+++ b/src/Tools/jEdit/patches/laf_fonts	Wed May 21 15:09:48 2025 +0200
@@ -12,4 +12,3 @@
  
  		// This is handled a little differently from other jEdit settings
  		// as this flag needs to be known very early in the
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java