tuned whitespace;
authorwenzelm
Tue, 05 Jan 2021 19:34:32 +0100
changeset 73067 d045d900a929
parent 73066 27f79e7eb356
child 73068 a95f5ae5a12a
tuned whitespace;
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>