tuned message;
authorwenzelm
Wed, 10 Apr 2019 13:45:49 +0200
changeset 70103 a6236d5a89ae
parent 70102 e48ffba6b557
child 70104 e6b7729453bf
tuned message;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Apr 10 13:43:23 2019 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Apr 10 13:45:49 2019 +0200
@@ -497,7 +497,7 @@
         // build heaps
 
         if (build_sessions.nonEmpty) {
-          progress.echo("Building " + commas(build_sessions) + " ...")
+          progress.echo("Building heaps ...")
           remote_build_heaps(options, platform, build_sessions, isabelle_target)
         }