src/Pure/Tools/build.scala
changeset 62303 f868f12f9419
parent 62302 236e1ea5a197
child 62399 36e885190439
     1.1 --- a/src/Pure/Tools/build.scala	Sun Feb 14 11:52:27 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Feb 14 12:03:32 2016 +0100
     1.3 @@ -640,8 +640,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(Output.error_text("Timeout")).set_rc(1)
     1.8 -        else res.add_err(Output.error_text("Interrupt"))
     1.9 +        if (was_timeout) res.error(Output.error_text("Timeout"), 1)
    1.10 +        else res.error(Output.error_text("Interrupt"))
    1.11        }
    1.12        else res
    1.13      }