Admin/lib/Tools/makedist_bundle
changeset 62036 773cb226738c
parent 62033 e1a4d52d3d53
child 62037 9bb80149dad9
--- a/Admin/lib/Tools/makedist_bundle	Sat Jan 02 13:29:34 2016 +0100
+++ b/Admin/lib/Tools/makedist_bundle	Sat Jan 02 15:18:38 2016 +0100
@@ -201,6 +201,7 @@
         do
           echo "$ARG"
         done
+        echo "-Disabelle.jedit_server=${ISABELLE_NAME}"
       ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options${PLATFORM}"
     done
 
@@ -268,6 +269,7 @@
       do
         echo -e "$ARG\r"
       done
+      echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r"
     ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.l4j.ini"
 
     (
@@ -370,6 +372,7 @@
           do
             echo "<string>$OPT</string>"
           done
+          echo "<string>-Disabelle.jedit_server={ISABELLE_NAME}</string>"
           echo "<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>"
 
           cat "$APP_TEMPLATE/Info.plist-part2"