diff -r 876e7eae22be -r 2d3d26e9b191 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Sep 30 21:05:14 2015 +0200
+++ b/lib/scripts/getsettings	Wed Sep 30 21:32:44 2015 +0200
@@ -36,9 +36,9 @@
     USER_HOME="$(cygpath -u "$USERPROFILE")"
   fi
 
-  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
-  CYGWIN_ROOT="$(jvmpath "/")"
-  ISABELLE_ROOT="$(jvmpath "$ISABELLE_HOME")"
+  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
+  CYGWIN_ROOT="$(platform_path "/")"
+  ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
 
   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
   unset CLASSPATH
@@ -49,7 +49,7 @@
 
   ISABELLE_ROOT="$ISABELLE_HOME"
 
-  function jvmpath() { echo "$@"; }
+  function platform_path() { echo "$@"; }
 
   ISABELLE_CLASSPATH="$CLASSPATH"
   unset CLASSPATH