tuned;
authorwenzelm
Tue, 11 Oct 2016 17:00:20 +0200
changeset 64147 92066f8c6a54
parent 64146 b2486964b823
child 64148 bbf43b7c4d0d
tuned;
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
     )
     ;;