diff -r d8849cfad60f -r 2fd73a1a0937 src/Tools/jEdit/patches/putenv --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/putenv Thu Oct 25 22:42:17 2018 +0200 @@ -0,0 +1,51 @@ +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 @@ + static final Pattern winPattern = Pattern.compile(winPatternString); + + ++ private static Map 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) ++ { ++ 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 @@ + if (m.find()) + { + String varName = m.group(2); +- String expansion = System.getenv(varName); ++ String expansion = getenv(varName); + if (expansion != null) + return m.replaceFirst(expansion); + } +@@ -174,7 +188,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(); +@@ -184,7 +198,7 @@ + varName = varName.toUpperCase(); + String uparg = arg.toUpperCase(); + m = p.matcher(uparg); +- expansion = System.getenv(varName); ++ expansion = getenv(varName); + } + } + if (expansion != null) {