proper environment for variable folding;
authorwenzelm
Fri Oct 26 12:43:39 2018 +0200 (9 months ago)
changeset 6919196b633ac24f8
parent 69190 278b09a92ed6
child 69193 49b3bb663981
proper environment for variable folding;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/patches/putenv
     1.1 --- a/Admin/components/components.sha1	Thu Oct 25 23:44:07 2018 +0200
     1.2 +++ b/Admin/components/components.sha1	Fri Oct 26 12:43:39 2018 +0200
     1.3 @@ -135,6 +135,7 @@
     1.4  7bcb202e13358dd750e964b2f747664428b5d8b3  jedit_build-20180417.tar.gz
     1.5  23c8a05687d05a6937f7d600ac3aa19e3ce59c9c  jedit_build-20180504.tar.gz
     1.6  9c64ee0705e5284b507ca527196081979d689519  jedit_build-20181025.tar.gz
     1.7 +cfa65bf8720b9b798ffa0986bafbc8437f44f758  jedit_build-20181026.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	Thu Oct 25 23:44:07 2018 +0200
     2.2 +++ b/Admin/components/main	Fri Oct 26 12:43:39 2018 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  e-2.0-2
     2.5  isabelle_fonts-20180113
     2.6  jdk-11+28
     2.7 -jedit_build-20181025
     2.8 +jedit_build-20181026
     2.9  jfreechart-1.5.0
    2.10  jortho-1.0-2
    2.11  kodkodi-1.5.2-1
     3.1 --- a/src/Tools/jEdit/patches/putenv	Thu Oct 25 23:44:07 2018 +0200
     3.2 +++ b/src/Tools/jEdit/patches/putenv	Fri Oct 26 12:43:39 2018 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
     3.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2018-04-09 01:57:06.000000000 +0200
     3.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2018-10-25 22:06:22.258705636 +0200
     3.7 -@@ -126,6 +126,20 @@
     3.8 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2018-10-26 12:29:44.315185808 +0200
     3.9 +@@ -126,6 +126,21 @@
    3.10   	static final Pattern winPattern = Pattern.compile(winPatternString);
    3.11   
    3.12   
    3.13 @@ -15,14 +15,15 @@
    3.14  +
    3.15  +	public static void putenv(String varName, String value)
    3.16  +	{
    3.17 -+		environ.put(varName, value);
    3.18 ++		if (value == null) environ.remove(varName);
    3.19 ++		else environ.put(varName, value);
    3.20  +	}
    3.21  +	
    3.22  +
    3.23   	/** A helper function for expandVariables when handling Windows paths on non-windows systems.
    3.24   	*/
    3.25   	private static String win2unix(String winPath)
    3.26 -@@ -135,7 +149,7 @@
    3.27 +@@ -135,7 +150,7 @@
    3.28   		if (m.find())
    3.29   		{
    3.30   			String varName = m.group(2);
    3.31 @@ -31,7 +32,7 @@
    3.32   			if (expansion != null)
    3.33   				return m.replaceFirst(expansion);
    3.34   		}
    3.35 -@@ -174,7 +188,7 @@
    3.36 +@@ -174,7 +189,7 @@
    3.37   				return arg;
    3.38   		}
    3.39   		String varName = m.group(2);
    3.40 @@ -40,7 +41,7 @@
    3.41   		if (expansion == null) {
    3.42   			if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
    3.43   				expansion = jEdit.getSettingsDirectory();
    3.44 -@@ -184,7 +198,7 @@
    3.45 +@@ -184,7 +199,7 @@
    3.46   				varName = varName.toUpperCase();
    3.47   				String uparg = arg.toUpperCase();
    3.48   				m = p.matcher(uparg);
    3.49 @@ -49,3 +50,18 @@
    3.50   			}
    3.51   		}
    3.52   		if (expansion != null) {
    3.53 +@@ -1637,13 +1652,11 @@
    3.54 + 		//{{{ VarCompressor constructor
    3.55 + 		VarCompressor()
    3.56 + 		{
    3.57 +-			ProcessBuilder pb = new ProcessBuilder();
    3.58 +-			Map<String, String> env = pb.environment();
    3.59 + 			if (OperatingSystem.isUnix())
    3.60 + 				prefixMap.put(System.getProperty("user.home"), "~");
    3.61 + 			if (jEdit.getSettingsDirectory() != null)
    3.62 + 				prefixMap.put(jEdit.getSettingsDirectory(), "JEDIT_SETTINGS");
    3.63 +-			for (Map.Entry<String, String> entry: env.entrySet())
    3.64 ++			for (Map.Entry<String, String> entry: environ.entrySet())
    3.65 + 			{
    3.66 + 				String k = entry.getKey();
    3.67 + 				if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;