# HG changeset patch
# User wenzelm
# Date 1406290399 -7200
# Node ID d7e22be79eb21b218a6d34e559a242325e16e217
# Parent  2f46999395e233f42f1d7d943ba5eee1a2b1d1c8
setup for drag-and-drop DMG;

diff -r 2f46999395e2 -r d7e22be79eb2 Admin/MacOS/dmg/DS_Store
Binary file Admin/MacOS/dmg/DS_Store has changed
diff -r 2f46999395e2 -r d7e22be79eb2 Admin/MacOS/dmg/background.png
Binary file Admin/MacOS/dmg/background.png has changed
diff -r 2f46999395e2 -r d7e22be79eb2 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Fri Jul 25 13:22:37 2014 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Fri Jul 25 14:13:19 2014 +0200
@@ -261,7 +261,12 @@
         cd "$TMP"
 
         APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
-        APP="${ISABELLE_NAME}.app"
+        APP="dmg/${ISABELLE_NAME}.app"
+
+        mkdir -p "dmg/.background"
+        cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/"
+        cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store"
+        ln -s /Applications "dmg/."
 
         for NAME in Java MacOS PlugIns Resources
         do
@@ -299,7 +304,9 @@
         ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
 
         rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
-        hdiutil create -srcfolder "$APP" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+
+        cd dmg
+        hdiutil create -srcfolder . -volname "$ISABELLE_NAME" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
       )
       ;;
     windows)