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