no censorship of view title;
authorwenzelm
Fri May 04 21:46:58 2018 +0200 (15 months ago)
changeset 680813d8f34715013
parent 68080 17f79ae49401
child 68082 b25ccd85b1fd
no censorship of view title;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/patches/title
     1.1 --- a/Admin/components/components.sha1	Fri May 04 16:22:09 2018 +0200
     1.2 +++ b/Admin/components/components.sha1	Fri May 04 21:46:58 2018 +0200
     1.3 @@ -126,6 +126,7 @@
     1.4  d4e1496c257659cf15458d718f4663cdd95a404e  jedit_build-20161024.tar.gz
     1.5  d806c1c26b571b5b4ef05ea11e8b9cf936518e06  jedit_build-20170319.tar.gz
     1.6  7bcb202e13358dd750e964b2f747664428b5d8b3  jedit_build-20180417.tar.gz
     1.7 +23c8a05687d05a6937f7d600ac3aa19e3ce59c9c  jedit_build-20180504.tar.gz
     1.8  0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
     1.9  8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
    1.10  d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
     2.1 --- a/Admin/components/main	Fri May 04 16:22:09 2018 +0200
     2.2 +++ b/Admin/components/main	Fri May 04 21:46:58 2018 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  e-2.0-1
     2.5  isabelle_fonts-20180113
     2.6  jdk-8u172
     2.7 -jedit_build-20180417
     2.8 +jedit_build-20180504
     2.9  jfreechart-1.5.0
    2.10  jortho-1.0-2
    2.11  kodkodi-1.5.2
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/patches/title	Fri May 04 21:46:58 2018 +0200
     3.3 @@ -0,0 +1,23 @@
     3.4 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/View.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java
     3.5 +--- 5.5.0/jEdit/org/gjt/sp/jedit/View.java	2018-04-09 01:57:31.000000000 +0200
     3.6 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java	2018-05-04 21:18:11.891194939 +0200
     3.7 +@@ -1233,15 +1233,10 @@
     3.8 + 
     3.9 + 		StringBuilder title = new StringBuilder();
    3.10 + 
    3.11 +-		/* On Mac OS X, apps are not supposed to show their name in the
    3.12 +-		title bar. */
    3.13 +-		if(!OperatingSystem.isMacOS())
    3.14 +-		{
    3.15 +-			if (userTitle != null)
    3.16 +-				title.append(userTitle);
    3.17 +-			else
    3.18 +-				title.append(jEdit.getProperty("view.title"));
    3.19 +-		}
    3.20 ++		if (userTitle != null)
    3.21 ++			title.append(userTitle);
    3.22 ++		else
    3.23 ++			title.append(jEdit.getProperty("view.title"));
    3.24 + 
    3.25 + 		for(int i = 0; i < buffers.size(); i++)
    3.26 + 		{