changeset 61293 | 876e7eae22be |
parent 61159 | da900891ee06 |
child 61294 | 2d3d26e9b191 |
--- a/lib/scripts/getsettings Wed Sep 30 20:48:59 2015 +0200 +++ b/lib/scripts/getsettings Wed Sep 30 21:05:14 2015 +0200 @@ -38,6 +38,7 @@ function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } CYGWIN_ROOT="$(jvmpath "/")" + ISABELLE_ROOT="$(jvmpath "$ISABELLE_HOME")" ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" unset CLASSPATH @@ -46,6 +47,8 @@ USER_HOME="$HOME" fi + ISABELLE_ROOT="$ISABELLE_HOME" + function jvmpath() { echo "$@"; } ISABELLE_CLASSPATH="$CLASSPATH"