THIS_CYGWIN;
authorwenzelm
Sat Apr 17 21:01:55 2010 +0200 (2010-04-17)
changeset 361948e61560ded89
parent 36193 067a01827fca
child 36195 9c098598db2a
THIS_CYGWIN;
lib/scripts/getsettings
src/Pure/System/cygwin.scala
     1.1 --- a/lib/scripts/getsettings	Sat Apr 17 20:42:26 2010 +0200
     1.2 +++ b/lib/scripts/getsettings	Sat Apr 17 21:01:55 2010 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  if [ "$OSTYPE" = cygwin ]; then
     1.5    CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
     1.6    function jvmpath() { cygpath -w -p "$@"; }
     1.7 -  CYGWIN_ROOT="$(jvmpath "/")"
     1.8 +  THIS_CYGWIN="$(jvmpath "/")"
     1.9  else
    1.10    function jvmpath() { echo "$@"; }
    1.11  fi
     2.1 --- a/src/Pure/System/cygwin.scala	Sat Apr 17 20:42:26 2010 +0200
     2.2 +++ b/src/Pure/System/cygwin.scala	Sat Apr 17 21:01:55 2010 +0200
     2.3 @@ -91,9 +91,9 @@
     2.4  
     2.5    def check_root(): String =
     2.6    {
     2.7 -    val root_env = java.lang.System.getenv("CYGWIN_ROOT")
     2.8 +    val this_cygwin = java.lang.System.getenv("THIS_CYGWIN")
     2.9      val root =
    2.10 -      if (root_env != null && root_env != "") root_env
    2.11 +      if (this_cygwin != null && this_cygwin != "") this_cygwin
    2.12        else
    2.13          query_registry(CYGWIN_SETUP1, "rootdir") orElse
    2.14          query_registry(CYGWIN_SETUP2, "rootdir") getOrElse