Admin/lib/Tools/makedist_bundle
changeset 53488 009d3bcf6907
parent 53485 a837df2ceee5
child 53489 97222a86aec0
--- a/Admin/lib/Tools/makedist_bundle	Mon Sep 09 16:15:48 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Mon Sep 09 17:02:06 2013 +0200
@@ -219,8 +219,18 @@
           mkdir -p "$APP/Contents/$NAME"
         done
 
-        cat "$APP_TEMPLATE/Info.plist" | \
-          perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
+        (
+          cat "$APP_TEMPLATE/Info.plist-part1"
+
+          declare -a OPTIONS=()
+          eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
+          for OPT in "${OPTIONS[@]}"
+          do
+            echo "<string>$OPT</string>"
+          done
+
+          cat "$APP_TEMPLATE/Info.plist-part2"
+        ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
 
         for NAME in Pure.jar scala-compiler.jar scala-library.jar scala-swing.jar scala-actors.jar scala-reflect.jar
         do