# HG changeset patch
# User wenzelm
# Date 1525463218 -7200
# Node ID 3d8f34715013a05b171e1051de8745d8357bd477
# Parent  17f79ae494013dbab9f99b578a1e188dc9593ce5
no censorship of view title;

diff -r 17f79ae49401 -r 3d8f34715013 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri May 04 16:22:09 2018 +0200
+++ b/Admin/components/components.sha1	Fri May 04 21:46:58 2018 +0200
@@ -126,6 +126,7 @@
 d4e1496c257659cf15458d718f4663cdd95a404e  jedit_build-20161024.tar.gz
 d806c1c26b571b5b4ef05ea11e8b9cf936518e06  jedit_build-20170319.tar.gz
 7bcb202e13358dd750e964b2f747664428b5d8b3  jedit_build-20180417.tar.gz
+23c8a05687d05a6937f7d600ac3aa19e3ce59c9c  jedit_build-20180504.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
diff -r 17f79ae49401 -r 3d8f34715013 Admin/components/main
--- a/Admin/components/main	Fri May 04 16:22:09 2018 +0200
+++ b/Admin/components/main	Fri May 04 21:46:58 2018 +0200
@@ -6,7 +6,7 @@
 e-2.0-1
 isabelle_fonts-20180113
 jdk-8u172
-jedit_build-20180417
+jedit_build-20180504
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.2
diff -r 17f79ae49401 -r 3d8f34715013 src/Tools/jEdit/patches/title
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/title	Fri May 04 21:46:58 2018 +0200
@@ -0,0 +1,23 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/View.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/View.java	2018-04-09 01:57:31.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java	2018-05-04 21:18:11.891194939 +0200
+@@ -1233,15 +1233,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++)
+ 		{