# HG changeset patch
# User wenzelm
# Date 1621173913 -7200
# Node ID 08def1cc6b337135f24fefdef27e23a4d2b8ecbf
# Parent  7202e12cb3241b387eaa3ef55033cdd45cfb9a6d
avoid perl;

diff -r 7202e12cb324 -r 08def1cc6b33 src/Pure/Admin/build_release.scala
--- 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"