equal
deleted
inserted
replaced
9 |
9 |
10 set -o allexport |
10 set -o allexport |
11 |
11 |
12 ISABELLE_SETTINGS_PRESENT=true |
12 ISABELLE_SETTINGS_PRESENT=true |
13 |
13 |
14 #JVM path wrapper |
14 #Cygwin vs Posix |
15 if [ "$OSTYPE" = cygwin ] |
15 if [ "$OSTYPE" = cygwin ] |
16 then |
16 then |
|
17 if [ -z "$USER_HOME" ]; then |
|
18 USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")" |
|
19 fi |
|
20 |
17 ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")" |
21 ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")" |
18 ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")" |
22 ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")" |
19 |
23 |
20 CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
24 CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
21 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
25 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
22 THIS_CYGWIN="$(jvmpath "/")" |
26 THIS_CYGWIN="$(jvmpath "/")" |
23 else |
27 else |
|
28 if [ -z "$USER_HOME" ]; then |
|
29 USER_HOME="$HOME" |
|
30 fi |
|
31 |
24 function jvmpath() { echo "$@"; } |
32 function jvmpath() { echo "$@"; } |
25 CLASSPATH="$CLASSPATH" |
33 CLASSPATH="$CLASSPATH" |
26 fi |
34 fi |
27 HOME_JVM="$HOME" |
|
28 |
35 |
29 export ISABELLE_HOME |
36 export ISABELLE_HOME |
30 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; } |
37 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; } |
31 then |
38 then |
32 echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!" |
39 echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!" |