# HG changeset patch
# User wenzelm
# Date 1456356477 -3600
# Node ID d653532762e4670725b8d71713467488e72f56f0
# Parent  13a0f537e232884a2346d5eed8ba683a304b7949
proper return code for timeout (amending f868f12f9419);

diff -r 13a0f537e232 -r d653532762e4 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Thu Feb 25 00:18:48 2016 +0100
+++ b/src/Pure/System/process_result.scala	Thu Feb 25 00:27:57 2016 +0100
@@ -14,11 +14,9 @@
 {
   def out: String = cat_lines(out_lines)
   def err: String = cat_lines(err_lines)
+  def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
 
-  def error(s: String, err_rc: Int = 0): Process_Result =
-    copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
-
-  def set_timeout(t: Time): Process_Result = copy(timeout = Some(t))
+  def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
 
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code
diff -r 13a0f537e232 -r d653532762e4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Feb 25 00:18:48 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:27:57 2016 +0100
@@ -642,7 +642,7 @@
 
       if (res.interrupted) {
         was_timeout match {
-          case Some(t) => res.error(Output.error_text("Timeout"), 1).set_timeout(t)
+          case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
           case None => res.error(Output.error_text("Interrupt"))
         }
       }