equal
deleted
inserted
replaced
49 |
49 |
50 #JVM path wrapper |
50 #JVM path wrapper |
51 if [ "$OSTYPE" = cygwin ]; then |
51 if [ "$OSTYPE" = cygwin ]; then |
52 CLASSPATH="$(cygpath -u -p "$CLASSPATH")" |
52 CLASSPATH="$(cygpath -u -p "$CLASSPATH")" |
53 function jvmpath() { cygpath -w -p "$@"; } |
53 function jvmpath() { cygpath -w -p "$@"; } |
54 ISABELLE_ROOT_JVM="$(jvmpath /)" |
|
55 else |
54 else |
56 function jvmpath() { echo "$@"; } |
55 function jvmpath() { echo "$@"; } |
57 ISABELLE_ROOT_JVM=/ |
|
58 fi |
56 fi |
59 HOME_JVM="$HOME" |
57 HOME_JVM="$HOME" |
60 |
58 |
61 #CLASSPATH convenience |
59 #CLASSPATH convenience |
62 function classpath () { |
60 function classpath () { |