THIS_CYGWIN;
authorwenzelm
Sat, 17 Apr 2010 21:01:55 +0200
changeset 36194 8e61560ded89
parent 36193 067a01827fca
child 36195 9c098598db2a
THIS_CYGWIN;
lib/scripts/getsettings
src/Pure/System/cygwin.scala
--- a/lib/scripts/getsettings	Sat Apr 17 20:42:26 2010 +0200
+++ b/lib/scripts/getsettings	Sat Apr 17 21:01:55 2010 +0200
@@ -53,7 +53,7 @@
 if [ "$OSTYPE" = cygwin ]; then
   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
   function jvmpath() { cygpath -w -p "$@"; }
-  CYGWIN_ROOT="$(jvmpath "/")"
+  THIS_CYGWIN="$(jvmpath "/")"
 else
   function jvmpath() { echo "$@"; }
 fi
--- a/src/Pure/System/cygwin.scala	Sat Apr 17 20:42:26 2010 +0200
+++ b/src/Pure/System/cygwin.scala	Sat Apr 17 21:01:55 2010 +0200
@@ -91,9 +91,9 @@
 
   def check_root(): String =
   {
-    val root_env = java.lang.System.getenv("CYGWIN_ROOT")
+    val this_cygwin = java.lang.System.getenv("THIS_CYGWIN")
     val root =
-      if (root_env != null && root_env != "") root_env
+      if (this_cygwin != null && this_cygwin != "") this_cygwin
       else
         query_registry(CYGWIN_SETUP1, "rootdir") orElse
         query_registry(CYGWIN_SETUP2, "rootdir") getOrElse