# HG changeset patch
# User wenzelm
# Date 1406292458 -7200
# Node ID 648c5ef4876d59b103ae6cc2e8df2577e4caf080
# Parent  aabfd69ab7545aea2fe683210040a22125a22926
proper volume name, such that background image is found in /Volumes/Isabelle/.background;

diff -r aabfd69ab754 -r 648c5ef4876d Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Fri Jul 25 14:16:39 2014 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Fri Jul 25 14:47:38 2014 +0200
@@ -306,7 +306,7 @@
         rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
 
         cd dmg
-        hdiutil create -srcfolder . -volname "$ISABELLE_NAME" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+        hdiutil create -srcfolder . -volname Isabelle "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
       )
       ;;
     windows)