equal
deleted
inserted
replaced
305 source "$COMPONENT/etc/settings" |
305 source "$COMPONENT/etc/settings" |
306 |
306 |
307 |
307 |
308 # main |
308 # main |
309 |
309 |
310 declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) |
310 declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options")) |
311 |
311 |
312 "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" |
312 "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" |
313 |
313 |
314 exec "$ISABELLE_JDK_HOME/bin/java" \ |
314 exec "$ISABELLE_JDK_HOME/bin/java" \ |
315 "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ |
315 "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ |