lib/scripts/getsettings
changeset 53967 bfaae48b0ce0
parent 53913 5ff12177a067
child 53970 eee1863c565a
--- a/lib/scripts/getsettings	Sat Sep 28 13:40:33 2013 +0200
+++ b/lib/scripts/getsettings	Sat Sep 28 13:50:38 2013 +0200
@@ -23,9 +23,6 @@
     USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
   fi
 
-  ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
-  ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
-
   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
   CYGWIN_ROOT="$(jvmpath "/")"