src/Tools/jEdit/patches/title
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 68081 3d8f34715013
permissions -rw-r--r--
formal update of patches -- no change of content;
     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	2019-02-24 12:21:17.050704937 +0100
     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  		{