author | wenzelm |
Sun, 16 May 2021 16:05:13 +0200 | |
changeset 73703 | 08def1cc6b33 |
parent 73702 | 7202e12cb324 |
child 73704 | 7c7a59b76528 |
--- a/src/Pure/Admin/build_release.scala Sun May 16 13:34:27 2021 +0200 +++ b/src/Pure/Admin/build_release.scala Sun May 16 16:05:13 2021 +0200 @@ -307,7 +307,7 @@ # main -declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) +declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options")) "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"