# HG changeset patch
# User wenzelm
# Date 1476459310 -7200
# Node ID bee9d2609404714eee7da1eb0696d492cd937da3
# Parent  db9ac35cae0d06de3bf8662aff8aede18b18c915
tuned messages;

diff -r db9ac35cae0d -r bee9d2609404 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Fri Oct 14 17:31:08 2016 +0200
+++ b/src/Pure/Admin/build_release.scala	Fri Oct 14 17:35:10 2016 +0200
@@ -56,7 +56,7 @@
     val jobs_option = " -j" + parallel_jobs.toString
 
     if (release_info.dist_archive.is_file)
-      progress.echo("Release archive " + release_info.dist_archive + " already exists")
+      progress.echo("### Release archive already exists: " + release_info.dist_archive)
     else {
       progress.echo("Producing release archive " + release_info.dist_archive + " ...")
       progress.bash(
@@ -78,7 +78,7 @@
               release_info.name + "_dmg.tar.gz"
             else platform_bundle)
       if (bundle_archive.is_file)
-        progress.echo("Application bundle " + bundle_archive + " already exists")
+        progress.echo("### Application bundle already exists: " + bundle_archive)
       else {
         progress.echo("\n*** " + platform_family + ": " + bundle_archive + " ***")
         progress.bash(
@@ -117,7 +117,7 @@
 
     if (build_library) {
       if (release_info.dist_library_archive.is_file)
-        progress.echo("Library archive " + release_info.dist_library_archive + " already exists")
+        progress.echo("### Library archive already exists: " + release_info.dist_library_archive)
       else {
         progress.bash("\"$ISABELLE_HOME/Admin/Release/build_library\"" + jobs_option + " " +
           File.bash_path(release_info.dist_dir +