equal
deleted
inserted
replaced
7 CLASSPATH="$(jvmpath "$CLASSPATH")" |
7 CLASSPATH="$(jvmpath "$CLASSPATH")" |
8 |
8 |
9 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
9 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
10 if "$JAVA_EXE" -server >/dev/null 2>/dev/null |
10 if "$JAVA_EXE" -server >/dev/null 2>/dev/null |
11 then |
11 then |
12 exec "$JAVA_EXE" -server "$@" |
12 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 -server "$@" |
13 else |
13 else |
14 exec "$JAVA_EXE" "$@" |
14 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 "$@" |
15 fi |
15 fi |
16 |
16 |