src/Pure/Tools/build.scala
changeset 62405 d653532762e4
parent 62404 13a0f537e232
child 62406 b5b8fb87447a
     1.1 --- a/src/Pure/Tools/build.scala	Thu Feb 25 00:18:48 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:27:57 2016 +0100
     1.3 @@ -642,7 +642,7 @@
     1.4  
     1.5        if (res.interrupted) {
     1.6          was_timeout match {
     1.7 -          case Some(t) => res.error(Output.error_text("Timeout"), 1).set_timeout(t)
     1.8 +          case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
     1.9            case None => res.error(Output.error_text("Interrupt"))
    1.10          }
    1.11        }