# HG changeset patch
# User wenzelm
# Date 1610812934 -3600
# Node ID 8a8ffe78eee7cf96ac349bffe99bbdcd8a018244
# Parent  497e11537d48fc22775c5f8f5c7979092728bc26
clarified return code: re-use SIGALRM for soft timeout;

diff -r 497e11537d48 -r 8a8ffe78eee7 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Jan 16 15:43:54 2021 +0100
+++ b/src/Pure/System/bash.scala	Sat Jan 16 17:02:14 2021 +0100
@@ -199,7 +199,7 @@
 
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
+      Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
   }
 }
diff -r 497e11537d48 -r 8a8ffe78eee7 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Sat Jan 16 15:43:54 2021 +0100
+++ b/src/Pure/System/process_result.scala	Sat Jan 16 17:02:14 2021 +0100
@@ -26,14 +26,16 @@
       137 -> "KILL SIGNAL",
       138 -> "BUS ERROR",
       139 -> "SEGMENTATION VIOLATION",
+      142 -> "TIMEOUT",
       143 -> "TERMINATION SIGNAL")
+
+  val timeout_rc = 142
 }
 
 final case class Process_Result(
   rc: Int,
   out_lines: List[String] = Nil,
   err_lines: List[String] = Nil,
-  timeout: Boolean = false,
   timing: Timing = Timing.zero)
 {
   def out: String = cat_lines(out_lines)
@@ -46,11 +48,12 @@
   def error(err: String): Process_Result =
     if (err.isEmpty) this else errors(List(err))
 
-  def was_timeout: Process_Result = copy(rc = 1, timeout = true)
-
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code
 
+  def timeout_rc: Process_Result = copy(rc = Process_Result.timeout_rc)
+  def timeout: Boolean = rc == Process_Result.timeout_rc
+
   def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
 
   def errors_rc(errs: List[String]): Process_Result =
diff -r 497e11537d48 -r 8a8ffe78eee7 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Jan 16 15:43:54 2021 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Jan 16 17:02:14 2021 +0100
@@ -523,10 +523,9 @@
       }
 
     val result2 =
-      if (result1.interrupted) {
-        if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
-        else result1.error(Output.error_message_text("Interrupt"))
-      }
+      if (result1.ok) result1
+      else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc
+      else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
       else result1
 
     val heap_digest =