# HG changeset patch
# User wenzelm
# Date 1621163173 -7200
# Node ID 908351c8c0b1f009eb3e2d1368a8ca82f324e61e
# Parent  c74e25de3c0092ab5e69d4f52900ca6412414995
check timeout_ignored as in ML, before applying timeout_scale;

diff -r c74e25de3c00 -r 908351c8c0b1 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat May 15 22:39:07 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun May 16 13:06:13 2021 +0200
@@ -502,6 +502,7 @@
 
     def dirs: List[Path] = dir :: directories
 
+    def timeout_ignored: Boolean = Time.seconds(options.real("timeout")) < Time.ms(1)
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def document_enabled: Boolean =
diff -r c74e25de3c00 -r 908351c8c0b1 src/Pure/Tools/build_job.scala
--- 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]) =