equal
deleted
inserted
replaced
209 chmod +x "$APP/Contents/MacOS/JavaAppLauncher" |
209 chmod +x "$APP/Contents/MacOS/JavaAppLauncher" |
210 |
210 |
211 mv "$ISABELLE_NAME" "$APP/Contents/Resources/." |
211 mv "$ISABELLE_NAME" "$APP/Contents/Resources/." |
212 ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle" |
212 ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle" |
213 |
213 |
|
214 rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" |
214 hdiutil create -srcfolder "$APP" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" |
215 hdiutil create -srcfolder "$APP" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" |
215 ) |
216 ) |
216 ;; |
217 ;; |
217 windows) |
218 windows) |
218 ( |
219 ( |