| changeset 69126 | e1b4b14ded58 |
| parent 67490 | 982f0bf34804 |
| child 73705 | ac07f6be27ea |
| 69125:60b6c759134f | 69126:e1b4b14ded58 |
|---|---|
65 exit 127 |
65 exit 127 |
66 else |
66 else |
67 unset ISABELLE_HOME |
67 unset ISABELLE_HOME |
68 unset CLASSPATH |
68 unset CLASSPATH |
69 exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \ |
69 exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \ |
70 "-Djava.ext.dirs=$JAVA_HOME/lib/ext" \ |
|
71 -classpath "$ISABELLE_CLASSPATH" "$@" |
70 -classpath "$ISABELLE_CLASSPATH" "$@" |
72 fi |
71 fi |
73 } |
72 } |