lib/scripts/getsettings
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"