proper return code for timeout (amending f868f12f9419);
authorwenzelm
Thu Feb 25 00:27:57 2016 +0100 (2016-02-25)
changeset 62405d653532762e4
parent 62404 13a0f537e232
child 62406 b5b8fb87447a
proper return code for timeout (amending f868f12f9419);
src/Pure/System/process_result.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/System/process_result.scala	Thu Feb 25 00:18:48 2016 +0100
     1.2 +++ b/src/Pure/System/process_result.scala	Thu Feb 25 00:27:57 2016 +0100
     1.3 @@ -14,11 +14,9 @@
     1.4  {
     1.5    def out: String = cat_lines(out_lines)
     1.6    def err: String = cat_lines(err_lines)
     1.7 +  def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
     1.8  
     1.9 -  def error(s: String, err_rc: Int = 0): Process_Result =
    1.10 -    copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
    1.11 -
    1.12 -  def set_timeout(t: Time): Process_Result = copy(timeout = Some(t))
    1.13 +  def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
    1.14  
    1.15    def ok: Boolean = rc == 0
    1.16    def interrupted: Boolean = rc == Exn.Interrupt.return_code
     2.1 --- a/src/Pure/Tools/build.scala	Thu Feb 25 00:18:48 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:27:57 2016 +0100
     2.3 @@ -642,7 +642,7 @@
     2.4  
     2.5        if (res.interrupted) {
     2.6          was_timeout match {
     2.7 -          case Some(t) => res.error(Output.error_text("Timeout"), 1).set_timeout(t)
     2.8 +          case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
     2.9            case None => res.error(Output.error_text("Interrupt"))
    2.10          }
    2.11        }