Admin/lib/Tools/makedist_bundle
changeset 66906 03a96b8c7c06
parent 66726 5223317b8c56
child 66908 9b074f01a305
equal deleted inserted replaced
66904:d9783ea1160c 66906:03a96b8c7c06
   189   "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
   189   "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
   190 
   190 
   191 case "$PLATFORM_FAMILY" in
   191 case "$PLATFORM_FAMILY" in
   192   linux)
   192   linux)
   193     purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
   193     purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
   194     purge_jdk "x86-linux"
       
   195     purge_jdk "x86_64-linux"
   194     purge_jdk "x86_64-linux"
   196 
   195 
   197     for PLATFORM in 32 64
   196     (
   198     do
   197       init_component "$JEDIT_HOME"
   199       (
   198 
   200         init_component "$JEDIT_HOME"
   199       echo "# Java runtime options"
   201 
   200       eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   202         echo "# Java runtime options for ${PLATFORM}bit platform"
   201       for ARG in "${JAVA_ARGS[@]}"
   203         declare -a JAVA_ARGS
   202       do
   204         if [ "$PLATFORM" = 32 ]; then
   203         echo "$ARG"
   205           eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS32)"
   204       done
   206         else
   205       echo "-Disabelle.jedit_server=${ISABELLE_NAME}"
   207           eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS64)"
   206     ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options"
   208         fi
       
   209         for ARG in "${JAVA_ARGS[@]}"
       
   210         do
       
   211           echo "$ARG"
       
   212         done
       
   213         echo "-Disabelle.jedit_server=${ISABELLE_NAME}"
       
   214       ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options${PLATFORM}"
       
   215     done
       
   216 
   207 
   217     LINUX_CLASSPATH=""
   208     LINUX_CLASSPATH=""
   218     for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
   209     for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
   219     do
   210     do
   220       if [ -z "$LINUX_CLASSPATH" ]; then
   211       if [ -z "$LINUX_CLASSPATH" ]; then
   256       "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
   247       "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
   257 
   248 
   258     (
   249     (
   259       init_component "$JEDIT_HOME"
   250       init_component "$JEDIT_HOME"
   260 
   251 
   261       declare -a JAVA_ARGS=()
   252       echo -e "# Java runtime options\r"
   262       echo -e "# Java runtime options for 64bit platform\r"
   253       eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   263       eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS64)"
       
   264       for ARG in "${JAVA_ARGS[@]}"
   254       for ARG in "${JAVA_ARGS[@]}"
   265       do
   255       do
   266         echo -e "$ARG\r"
   256         echo -e "$ARG\r"
   267       done
   257       done
   268       echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r"
   258       echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r"
   364         init_component "$JEDIT_HOME"
   354         init_component "$JEDIT_HOME"
   365 
   355 
   366         cat "$APP_TEMPLATE/Info.plist-part1"
   356         cat "$APP_TEMPLATE/Info.plist-part1"
   367 
   357 
   368         declare -a OPTIONS=()
   358         declare -a OPTIONS=()
   369         eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS64)"
   359         eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   370         for OPT in "${OPTIONS[@]}"
   360         for OPT in "${OPTIONS[@]}"
   371         do
   361         do
   372           echo "<string>$OPT</string>"
   362           echo "<string>$OPT</string>"
   373         done
   363         done
   374         echo "<string>-Disabelle.jedit_server={ISABELLE_NAME}</string>"
   364         echo "<string>-Disabelle.jedit_server={ISABELLE_NAME}</string>"