diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2020-09-08 20:13:35.648786692 +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;