lib/scripts/getsettings
changeset 61294 2d3d26e9b191
parent 61293 876e7eae22be
child 61319 d84b4d39bce1
     1.1 --- a/lib/scripts/getsettings	Wed Sep 30 21:05:14 2015 +0200
     1.2 +++ b/lib/scripts/getsettings	Wed Sep 30 21:32:44 2015 +0200
     1.3 @@ -36,9 +36,9 @@
     1.4      USER_HOME="$(cygpath -u "$USERPROFILE")"
     1.5    fi
     1.6  
     1.7 -  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
     1.8 -  CYGWIN_ROOT="$(jvmpath "/")"
     1.9 -  ISABELLE_ROOT="$(jvmpath "$ISABELLE_HOME")"
    1.10 +  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
    1.11 +  CYGWIN_ROOT="$(platform_path "/")"
    1.12 +  ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
    1.13  
    1.14    ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    1.15    unset CLASSPATH
    1.16 @@ -49,7 +49,7 @@
    1.17  
    1.18    ISABELLE_ROOT="$ISABELLE_HOME"
    1.19  
    1.20 -  function jvmpath() { echo "$@"; }
    1.21 +  function platform_path() { echo "$@"; }
    1.22  
    1.23    ISABELLE_CLASSPATH="$CLASSPATH"
    1.24    unset CLASSPATH