Admin/lib/Tools/makedist_bundle
changeset 66726 5223317b8c56
parent 66724 1e1f9f603385
child 66906 03a96b8c7c06
equal deleted inserted replaced
66725:c37c4f0db878 66726:5223317b8c56
   242       -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
   242       -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
   243       -e "s,plugin-blacklist.MacOSX.jar=true,plugin-blacklist.MacOSX.jar=,g;" \
   243       -e "s,plugin-blacklist.MacOSX.jar=true,plugin-blacklist.MacOSX.jar=,g;" \
   244       "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
   244       "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
   245     ;;
   245     ;;
   246   windows)
   246   windows)
   247     purge_target 'contrib -name "x86*-linux" -o -name "x86*-darwin"'
   247     purge_target 'contrib -name "x86*-linux" -o -name "x86*-darwin" -o -name "x86-cygwin"'
   248     purge_target 'contrib/jdk -name "x86-windows"'
   248     purge_target 'contrib/jdk -name "x86-windows"'
   249     purge_jdk "x86_64-windows"
   249     purge_jdk "x86_64-windows"
   250 
   250 
   251     mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
   251     mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
   252 
   252