equal
deleted
inserted
replaced
42 |
42 |
43 [ -z "$RESULT" ] && RESULT="$FILE" |
43 [ -z "$RESULT" ] && RESULT="$FILE" |
44 echo "$RESULT" |
44 echo "$RESULT" |
45 } |
45 } |
46 |
46 |
47 #JVM path wrappers |
47 #JVM path wrapper |
48 if [ "$OSTYPE" = cygwin ]; then |
48 if [ "$OSTYPE" = cygwin ]; then |
49 CLASSPATH="$(cygpath -u -p "$CLASSPATH")" |
49 CLASSPATH="$(cygpath -u -p "$CLASSPATH")" |
50 function jvmpath() { cygpath -w -p "$@"; } |
50 function jvmpath() { cygpath -w -p "$@"; } |
51 function javawrapper() { env CLASSPATH="$(jvmpath "$CLASSPATH")" java "$@"; } |
|
52 function scalawrapper() { env CLASSPATH="$(jvmpath "$CLASSPATH")" scala "$@"; } |
|
53 else |
51 else |
54 function jvmpath() { echo "$@"; } |
52 function jvmpath() { echo "$@"; } |
55 function javawrapper() { java "$@"; } |
|
56 function scalawrapper() { scala "$@"; } |
|
57 fi |
53 fi |
58 ISABELLE_HOME_JVM="$(jvmpath "$ISABELLE_HOME")" |
|
59 |
54 |
60 #CLASSPATH convenience |
55 #CLASSPATH convenience |
61 function classpath () { |
56 function classpath () { |
62 for X in "$@" |
57 for X in "$@" |
63 do |
58 do |
85 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
80 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
86 fi |
81 fi |
87 |
82 |
88 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
83 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
89 |
84 |
|
85 #JVM settings |
|
86 ISABELLE_HOME_JVM="$(jvmpath "$ISABELLE_HOME")" |
|
87 ISABELLE_HOME_USER_JVM="$(jvmpath "$ISABELLE_HOME_USER")" |
|
88 |
90 set +o allexport |
89 set +o allexport |
91 |
90 |
92 fi |
91 fi |