src/Pure/Tools/build.scala
changeset 65828 02dd430d80c5
parent 65827 3bba3856b56c
child 65831 3b197547c1d4
     1.1 --- a/src/Pure/Tools/build.scala	Sun May 14 17:01:05 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sun May 14 17:05:06 2017 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4              case msg =>
     1.5                result.copy(
     1.6                  rc = result.rc max 1,
     1.7 -                out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
     1.8 +                out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
     1.9            }
    1.10          }
    1.11          else {
    1.12 @@ -309,8 +309,8 @@
    1.13        timeout_request.foreach(_.cancel)
    1.14  
    1.15        if (result.interrupted) {
    1.16 -        if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
    1.17 -        else result.error(Output.error_text("Interrupt"))
    1.18 +        if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
    1.19 +        else result.error(Output.error_message_text("Interrupt"))
    1.20        }
    1.21        else result
    1.22      }