--- 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++)
+ {
--- 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++)
- {