changeset 43521 | d477b92109b8 |
parent 43518 | 7cad71ca9bcc |
child 43522 | 2562d6c81b03 |
43520:cec9b95fa35d | 43521:d477b92109b8 |
---|---|
34 |
34 |
35 |
35 |
36 ## main |
36 ## main |
37 |
37 |
38 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
38 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
39 exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs "$@" |
39 exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \ |
40 "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" |
|
40 |
41 |