src/Tools/jEdit/patches/title
author wenzelm
Fri May 04 21:46:58 2018 +0200 (13 months ago ago)
changeset 68081 3d8f34715013
child 70019 4419d4d675c3
permissions -rw-r--r--
no censorship of view title;
     1 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/View.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java
     2 --- 5.5.0/jEdit/org/gjt/sp/jedit/View.java	2018-04-09 01:57:31.000000000 +0200
     3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java	2018-05-04 21:18:11.891194939 +0200
     4 @@ -1233,15 +1233,10 @@
     5  
     6  		StringBuilder title = new StringBuilder();
     7  
     8 -		/* On Mac OS X, apps are not supposed to show their name in the
     9 -		title bar. */
    10 -		if(!OperatingSystem.isMacOS())
    11 -		{
    12 -			if (userTitle != null)
    13 -				title.append(userTitle);
    14 -			else
    15 -				title.append(jEdit.getProperty("view.title"));
    16 -		}
    17 +		if (userTitle != null)
    18 +			title.append(userTitle);
    19 +		else
    20 +			title.append(jEdit.getProperty("view.title"));
    21  
    22  		for(int i = 0; i < buffers.size(); i++)
    23  		{