tuned;

--- a/Admin/lib/Tools/makedist_bundle	Wed Oct 12 22:38:11 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Wed Oct 12 22:38:50 2016 +0200
@@ -423,10 +423,10 @@
 
       if [ -n "$REMOTE_MAC" ]
       then
-        echo -n "$REMOTE_MAC: building dmg ... "
+        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" &&
-          echo "done"
+          echo " done"
       fi
     )
     ;;