# HG changeset patch
# User wenzelm
# Date 1609871672 -3600
# Node ID d045d900a92917be66f8538e348850088a413fe4
# Parent  27f79e7eb356626cdbe6a975df165dcb3417ec90
tuned whitespace;

diff -r 27f79e7eb356 -r d045d900a929 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue Jan 05 19:18:57 2021 +0100
+++ b/src/Pure/Admin/build_release.scala	Tue Jan 05 19:34:32 2021 +0100
@@ -352,7 +352,7 @@
 </array>
 <key>JVMOptions</key>
 <array>
-""" + terminate_lines(java_options.map(opt => "<string>" + opt + "</string>")) + """
+""" + cat_lines(java_options.map(opt => "<string>" + opt + "</string>")) + """
 <string>-splash:$APP_ROOT/Contents/Resources/""" + isabelle_name + """/lib/logo/isabelle.gif</string>
 <string>-Dapple.awt.application.name=""" + isabelle_name + """</string>
 <string>-Disabelle.root=$APP_ROOT/Contents/Resources/""" + isabelle_name + """</string>