# HG changeset patch # User wenzelm # Date 1554896749 -7200 # Node ID a6236d5a89ae813998707830e0fd19b15a03f8cd # Parent e48ffba6b5573eaddfa8b977de2e4dc2f8775f19 tuned message; diff -r e48ffba6b557 -r a6236d5a89ae 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) }