changeset 73700 | 908351c8c0b1 |
parent 73559 | 22b5ecb53dd9 |
child 73718 | ecb31c3bf980 |
--- a/src/Pure/Tools/build_job.scala Sat May 15 22:39:07 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Sun May 16 13:06:13 2021 +0200 @@ -507,9 +507,8 @@ private val timeout_request: Option[Event_Timer.Request] = { - if (info.timeout > Time.zero) - Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) - else None + if (info.timeout_ignored) None + else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } def join: (Process_Result, Option[String]) =