equal
deleted
inserted
replaced
7 [ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } |
7 [ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } |
8 |
8 |
9 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } |
9 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } |
10 |
10 |
11 CLASSPATH="$(jvmpath "$CLASSPATH")" |
11 CLASSPATH="$(jvmpath "$CLASSPATH")" |
12 exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 "$@" |
12 exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \ |
|
13 "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@" |