equal
deleted
inserted
replaced
36 USER_HOME="$(cygpath -u "$USERPROFILE")" |
36 USER_HOME="$(cygpath -u "$USERPROFILE")" |
37 fi |
37 fi |
38 |
38 |
39 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
39 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
40 CYGWIN_ROOT="$(jvmpath "/")" |
40 CYGWIN_ROOT="$(jvmpath "/")" |
|
41 ISABELLE_ROOT="$(jvmpath "$ISABELLE_HOME")" |
41 |
42 |
42 ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
43 ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
43 unset CLASSPATH |
44 unset CLASSPATH |
44 else |
45 else |
45 if [ -z "$USER_HOME" ]; then |
46 if [ -z "$USER_HOME" ]; then |
46 USER_HOME="$HOME" |
47 USER_HOME="$HOME" |
47 fi |
48 fi |
|
49 |
|
50 ISABELLE_ROOT="$ISABELLE_HOME" |
48 |
51 |
49 function jvmpath() { echo "$@"; } |
52 function jvmpath() { echo "$@"; } |
50 |
53 |
51 ISABELLE_CLASSPATH="$CLASSPATH" |
54 ISABELLE_CLASSPATH="$CLASSPATH" |
52 unset CLASSPATH |
55 unset CLASSPATH |