# HG changeset patch
# User wenzelm
# Date 1476304730 -7200
# Node ID 35644caa62a7f23fe212263baab69bcfcbc355f7
# Parent  8945293a9ed0da7b4490c4103fac721c7611a596
tuned;

diff -r 8945293a9ed0 -r 35644caa62a7 Admin/lib/Tools/makedist_bundle
--- 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
     )
     ;;