changeset 72440 | d0ba71b3297e |
parent 72412 | 9ed9585c495b |
child 72444 | 2d9a70b85009 |
--- a/src/Pure/Admin/build_spass.scala Sun Oct 11 13:03:22 2020 +0200 +++ b/src/Pure/Admin/build_spass.scala Sun Oct 11 13:09:43 2020 +0200 @@ -79,7 +79,7 @@ /* build */ - progress.echo("Building SPASS ...") + progress.echo("Building SPASS for " + platform_name + " ...") val build_dir = tmp_dir + Path.basic(archive_base_name)