# HG changeset patch
# User wenzelm
# Date 1755862221 -7200
# Node ID d0da249ebd24e7ca178361a6c52104ccd07531cd
# Parent  393a15735a60a1d8851e0371744900ac294e4cdf
clarified patches: this is hardly modular anymore;

diff -r 393a15735a60 -r d0da249ebd24 src/Tools/jEdit/patches/main
--- a/src/Tools/jEdit/patches/main	Thu Aug 21 21:33:34 2025 +0200
+++ b/src/Tools/jEdit/patches/main	Fri Aug 22 13:30:21 2025 +0200
@@ -1326,3 +1326,25 @@
  
  		// This is handled a little differently from other jEdit settings
  		// as this flag needs to be known very early in the
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java	2024-10-29 11:50:54.066016546 +0100
+@@ -1264,15 +1264,10 @@
+ 
+ 		StringBuilder title = new StringBuilder();
+ 
+-		/* On Mac OS X, apps are not supposed to show their name in the
+-		title bar. */
+-		if(!OperatingSystem.isMacOS())
+-		{
+-			if (userTitle != null)
+-				title.append(userTitle);
+-			else
+-				title.append(jEdit.getProperty("view.title"));
+-		}
++		if (userTitle != null)
++			title.append(userTitle);
++		else
++			title.append(jEdit.getProperty("view.title"));
+ 
+ 		for(int i = 0; i < buffers.size(); i++)
+ 		{
diff -r 393a15735a60 -r d0da249ebd24 src/Tools/jEdit/patches/title
--- a/src/Tools/jEdit/patches/title	Thu Aug 21 21:33:34 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java	2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java	2024-10-29 11:50:54.066016546 +0100
-@@ -1264,15 +1264,10 @@
- 
- 		StringBuilder title = new StringBuilder();
- 
--		/* On Mac OS X, apps are not supposed to show their name in the
--		title bar. */
--		if(!OperatingSystem.isMacOS())
--		{
--			if (userTitle != null)
--				title.append(userTitle);
--			else
--				title.append(jEdit.getProperty("view.title"));
--		}
-+		if (userTitle != null)
-+			title.append(userTitle);
-+		else
-+			title.append(jEdit.getProperty("view.title"));
- 
- 		for(int i = 0; i < buffers.size(); i++)
- 		{