# HG changeset patch
# User wenzelm
# Date 1476198020 -7200
# Node ID 92066f8c6a549a43307041986d749c1992c19da6
# Parent  b2486964b823319630b6dcd6640867b5a9e9ae02
tuned;

diff -r b2486964b823 -r 92066f8c6a54 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Tue Oct 11 14:29:39 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Tue Oct 11 17:00:20 2016 +0200
@@ -422,9 +422,10 @@
 
       if [ -n "$REMOTE_MAC" ]
       then
-        echo "$REMOTE_MAC: dmg for $PLATFORM_FAMILY"
+        echo -n "$REMOTE_MAC: building dmg ... "
         isabelle remote_dmg -V Isabelle "$REMOTE_MAC" \
-          "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+          "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" &&
+          echo "done"
       fi
     )
     ;;