changeset 65827 | 3bba3856b56c |
parent 65532 | febfd9f78bd4 |
child 65828 | 02dd430d80c5 |
--- a/src/Pure/Tools/build.scala Sun May 14 17:00:57 2017 +0200 +++ b/src/Pure/Tools/build.scala Sun May 14 17:01:05 2017 +0200 @@ -551,7 +551,7 @@ val results0 = if (deps.is_empty) { - progress.echo(Output.warning_text("Nothing to build")) + progress.echo_warning("Nothing to build") Map.empty[String, Result] } else loop(queue, Map.empty, Map.empty)