author | wenzelm |
Wed, 10 Apr 2019 13:45:49 +0200 | |
changeset 70103 | a6236d5a89ae |
parent 70102 | e48ffba6b557 |
child 70104 | e6b7729453bf |
--- 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) }