Admin/lib/Tools/makedist_bundle
changeset 64147 92066f8c6a54
parent 64144 ef20d2da71af
child 64175 8945293a9ed0
--- 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
     )
     ;;