src/Pure/Tools/build.scala
changeset 56782 433cf57550fa
parent 56780 e76467fed375
child 56801 8dd9df88f647
     1.1 --- a/src/Pure/Tools/build.scala	Tue Apr 29 13:29:05 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 29 13:32:13 2014 +0200
     1.3 @@ -606,8 +606,8 @@
     1.4        timeout_request.foreach(_.cancel)
     1.5  
     1.6        if (res.rc == Exn.Interrupt.return_code) {
     1.7 -        if (was_timeout) res.add_err("*** Timeout").set_rc(1)
     1.8 -        else res.add_err("*** Interrupt")
     1.9 +        if (was_timeout) res.add_err(Output.error_text("Timeout")).set_rc(1)
    1.10 +        else res.add_err(Output.error_text("Interrupt"))
    1.11        }
    1.12        else res
    1.13      }
    1.14 @@ -758,8 +758,7 @@
    1.15  
    1.16        def ignore_error(msg: String): (List[Properties.T], Double) =
    1.17        {
    1.18 -        System.err.println("### Ignoring bad log file: " + path +
    1.19 -          (if (msg == "") "" else "\n" + msg))
    1.20 +        Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg))
    1.21          (Nil, 0.0)
    1.22        }
    1.23  
    1.24 @@ -902,7 +901,7 @@
    1.25  
    1.26      val results =
    1.27        if (deps.is_empty) {
    1.28 -        progress.echo("### Nothing to build")
    1.29 +        progress.echo(Output.warning_text("Nothing to build"))
    1.30          Map.empty[String, Result]
    1.31        }
    1.32        else loop(queue, Map.empty, Map.empty)