changeset 73700 | 908351c8c0b1 |
parent 73367 | 77ef8bef0593 |
child 73701 | d83e7e444b43 |
--- 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 =