# HG changeset patch
# User wenzelm
# Date 1540550619 -7200
# Node ID 96b633ac24f8c19e13826509b76841cce5790c51
# Parent  278b09a92ed6f05a559beb1493bd76284c49f83f
proper environment for variable folding;

diff -r 278b09a92ed6 -r 96b633ac24f8 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Oct 25 23:44:07 2018 +0200
+++ b/Admin/components/components.sha1	Fri Oct 26 12:43:39 2018 +0200
@@ -135,6 +135,7 @@
 7bcb202e13358dd750e964b2f747664428b5d8b3  jedit_build-20180417.tar.gz
 23c8a05687d05a6937f7d600ac3aa19e3ce59c9c  jedit_build-20180504.tar.gz
 9c64ee0705e5284b507ca527196081979d689519  jedit_build-20181025.tar.gz
+cfa65bf8720b9b798ffa0986bafbc8437f44f758  jedit_build-20181026.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 278b09a92ed6 -r 96b633ac24f8 Admin/components/main
--- a/Admin/components/main	Thu Oct 25 23:44:07 2018 +0200
+++ b/Admin/components/main	Fri Oct 26 12:43:39 2018 +0200
@@ -6,7 +6,7 @@
 e-2.0-2
 isabelle_fonts-20180113
 jdk-11+28
-jedit_build-20181025
+jedit_build-20181026
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.2-1
diff -r 278b09a92ed6 -r 96b633ac24f8 src/Tools/jEdit/patches/putenv
--- a/src/Tools/jEdit/patches/putenv	Thu Oct 25 23:44:07 2018 +0200
+++ b/src/Tools/jEdit/patches/putenv	Fri Oct 26 12:43:39 2018 +0200
@@ -1,7 +1,7 @@
 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
 --- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2018-04-09 01:57:06.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2018-10-25 22:06:22.258705636 +0200
-@@ -126,6 +126,20 @@
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2018-10-26 12:29:44.315185808 +0200
+@@ -126,6 +126,21 @@
  	static final Pattern winPattern = Pattern.compile(winPatternString);
  
  
@@ -15,14 +15,15 @@
 +
 +	public static void putenv(String varName, String value)
 +	{
-+		environ.put(varName, value);
++		if (value == null) environ.remove(varName);
++		else environ.put(varName, value);
 +	}
 +	
 +
  	/** A helper function for expandVariables when handling Windows paths on non-windows systems.
  	*/
  	private static String win2unix(String winPath)
-@@ -135,7 +149,7 @@
+@@ -135,7 +150,7 @@
  		if (m.find())
  		{
  			String varName = m.group(2);
@@ -31,7 +32,7 @@
  			if (expansion != null)
  				return m.replaceFirst(expansion);
  		}
-@@ -174,7 +188,7 @@
+@@ -174,7 +189,7 @@
  				return arg;
  		}
  		String varName = m.group(2);
@@ -40,7 +41,7 @@
  		if (expansion == null) {
  			if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
  				expansion = jEdit.getSettingsDirectory();
-@@ -184,7 +198,7 @@
+@@ -184,7 +199,7 @@
  				varName = varName.toUpperCase();
  				String uparg = arg.toUpperCase();
  				m = p.matcher(uparg);
@@ -49,3 +50,18 @@
  			}
  		}
  		if (expansion != null) {
+@@ -1637,13 +1652,11 @@
+ 		//{{{ VarCompressor constructor
+ 		VarCompressor()
+ 		{
+-			ProcessBuilder pb = new ProcessBuilder();
+-			Map<String, String> env = pb.environment();
+ 			if (OperatingSystem.isUnix())
+ 				prefixMap.put(System.getProperty("user.home"), "~");
+ 			if (jEdit.getSettingsDirectory() != null)
+ 				prefixMap.put(jEdit.getSettingsDirectory(), "JEDIT_SETTINGS");
+-			for (Map.Entry<String, String> entry: env.entrySet())
++			for (Map.Entry<String, String> entry: environ.entrySet())
+ 			{
+ 				String k = entry.getKey();
+ 				if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;