# HG changeset patch
# User wenzelm
# Date 1335116680 -7200
# Node ID c04b223d661e4c79c7d76a25b90f2e321bd48080
# Parent  4977297873a23e248a9b2509be9a3c9a54f94e3d# Parent  cdf95042e09cceafe5ebb8506b5cb73109769b3b
merged

diff -r 4977297873a2 -r c04b223d661e lib/Tools/getenv
--- a/lib/Tools/getenv	Sun Apr 22 19:18:26 2012 +0200
+++ b/lib/Tools/getenv	Sun Apr 22 19:44:40 2012 +0200
@@ -76,6 +76,7 @@
 fi
 
 if [ -n "$DUMP" ]; then
+  export PATH_JVM="$(jvmpath "$PATH")"
   exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
 fi
 
diff -r 4977297873a2 -r c04b223d661e lib/scripts/getsettings
diff -r 4977297873a2 -r c04b223d661e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Apr 22 19:18:26 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Apr 22 19:44:40 2012 +0200
@@ -74,12 +74,12 @@
               if (rc != 0) error(output)
 
               val entries =
-                for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
+                (for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
                   val i = entry.indexOf('=')
                   if (i <= 0) (entry -> "")
                   else (entry.substring(0, i) -> entry.substring(i + 1))
-                }
-              Map(entries: _*) + ("PATH" -> System.getenv("PATH"))
+                }).toMap
+              entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
             }
           }
       _state = Some(State(standard_system, settings))