| changeset 45385 | 7c1375ba1424 |
| parent 45105 | 21c09b727bf3 |
| child 47113 | b5a5662528fb |
| 45384:dffa657f0aa2 | 45385:7c1375ba1424 |
|---|---|
20 else |
20 else |
21 SERVER="" |
21 SERVER="" |
22 fi |
22 fi |
23 |
23 |
24 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \ |
24 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \ |
25 "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@" |
25 "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" |
26 |
26 |