# HG changeset patch
# User wenzelm
# Date 1262037457 -3600
# Node ID 99241daf807d27b95f6e6e4bf45e97edc53ac18f
# Parent  c95dcd12f48a22a40671e0d4fa3812ab3cc80c6f
ignore undefined environment;

diff -r c95dcd12f48a -r 99241daf807d src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Dec 28 22:03:14 2009 +0100
+++ b/src/Pure/System/standard_system.scala	Mon Dec 28 22:57:37 2009 +0100
@@ -107,8 +107,10 @@
     for (s <- args) cmdline.add(s)
 
     val proc = new ProcessBuilder(cmdline)
-    proc.environment.clear
-    for ((x, y) <- env) proc.environment.put(x, y)
+    if (env != null) {
+      proc.environment.clear
+      for ((x, y) <- env) proc.environment.put(x, y)
+    }
     proc.redirectErrorStream(redirect)
 
     try { proc.start }