src/Tools/jEdit/patches/putenv

updated NEWS

diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2021-05-10 11:23:04.139510558 +0200
@@ -131,6 +131,21 @@
 	static final Pattern winPattern = Pattern.compile(winPatternString);
 
 
+	private static Map<String,String> environ =
+		Collections.synchronizedMap(new HashMap(System.getenv()));
+
+	public static String getenv(String varName)
+	{
+		return environ.get(varName);
+	}
+
+	public static void putenv(String varName, String 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)
@@ -140,7 +155,7 @@
 		if (m.find())
 		{
 			String varName = m.group(2);
-			String expansion = System.getenv(varName);
+			String expansion = getenv(varName);
 			if (expansion != null)
 				return m.replaceFirst(expansion);
 		}
@@ -179,7 +194,7 @@
 				return arg;
 		}
 		String varName = m.group(2);
-		String expansion = System.getenv(varName);
+		String expansion = getenv(varName);
 		if (expansion == null) {
 			if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
 				expansion = jEdit.getSettingsDirectory();
@@ -189,7 +204,7 @@
 				varName = varName.toUpperCase();
 				String uparg = arg.toUpperCase();
 				m = p.matcher(uparg);
-				expansion = System.getenv(varName);
+				expansion = getenv(varName);
 			}
 		}
 		if (expansion != null) {
@@ -1682,13 +1697,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;