--- a/src/Pure/Thy/sessions.scala Sun May 16 13:06:13 2021 +0200
+++ b/src/Pure/Thy/sessions.scala Sun May 16 13:14:16 2021 +0200
@@ -502,7 +502,9 @@
def dirs: List[Path] = dir :: directories
- def timeout_ignored: Boolean = Time.seconds(options.real("timeout")) < Time.ms(1)
+ def timeout_ignored: Boolean =
+ !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
+
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
def document_enabled: Boolean =