# HG changeset patch
# User wenzelm
# Date 1476466974 -7200
# Node ID 5d5701bed047c4e11a8723084f2b3978eb7a45e8
# Parent  da9b04b8d2044849a28179d9955e2588f7d47b4a
tuned messages;

diff -r da9b04b8d204 -r 5d5701bed047 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Fri Oct 14 19:34:30 2016 +0200
+++ b/src/Pure/Admin/build_release.scala	Fri Oct 14 19:42:54 2016 +0200
@@ -59,9 +59,9 @@
     val jobs_option = " -j" + parallel_jobs.toString
 
     if (release_info.dist_archive.is_file)
-      progress.echo("### Release archive already exists: " + release_info.dist_archive)
+      progress.echo("### Release archive already exists: " + release_info.dist_archive.implode)
     else {
-      progress.echo("Producing release archive " + release_info.dist_archive + " ...")
+      progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...")
       progress.bash(
         "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
           (if (official_release) " -O" else "") +
@@ -79,9 +79,9 @@
           (if (remote_mac.isEmpty) fallback_platform_bundles.toMap.get(platform_family) else None)
             getOrElse platform_bundle)
       if (bundle_archive.is_file)
-        progress.echo("### Application bundle already exists: " + bundle_archive)
+        progress.echo("### Application bundle already exists: " + bundle_archive.implode)
       else {
-        progress.echo("\n*** " + platform_family + ": " + bundle_archive + " ***")
+        progress.echo("\nApplication bundle for " + platform_family + ": " + bundle_archive.implode)
         progress.bash(
           "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
             " " + File.bash_string(platform_family) +
@@ -126,7 +126,8 @@
 
     if (build_library) {
       if (release_info.dist_library_archive.is_file)
-        progress.echo("### Library archive already exists: " + release_info.dist_library_archive)
+        progress.echo("### Library archive already exists: " +
+          release_info.dist_library_archive.implode)
       else {
         progress.bash("\"$ISABELLE_HOME/Admin/Release/build_library\"" + jobs_option + " " +
           File.bash_path(release_info.dist_dir +