--- 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)
}
}
}
--- 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 =
--- 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 =