equal
deleted
inserted
replaced
12 ISABELLE_SETTINGS_PRESENT=true |
12 ISABELLE_SETTINGS_PRESENT=true |
13 |
13 |
14 #JVM path wrapper |
14 #JVM path wrapper |
15 if [ "$OSTYPE" = cygwin ] |
15 if [ "$OSTYPE" = cygwin ] |
16 then |
16 then |
17 ISABELLE_HOME_WINDOWS="$(cygpath -d "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")" |
17 ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")" |
18 ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")" |
18 ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")" |
19 |
19 |
20 CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
20 CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
21 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
21 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
22 THIS_CYGWIN="$(jvmpath "/")" |
22 THIS_CYGWIN="$(jvmpath "/")" |