src/Pure/Tools/server_commands.scala
changeset 68947 ea804c814693
parent 68943 e564605d4cac
child 69012 c91d14ab065f
     1.1 --- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 13:22:23 2018 +0200
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 13:36:40 2018 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4        export_pattern: String = "",
     1.5        check_delay: Time = Thy_Resources.default_check_delay,
     1.6        check_limit: Int = 0,
     1.7 -      watchdog_timeout: Time = Time.zero,
     1.8 +      watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
     1.9        nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
    1.10  
    1.11      def unapply(json: JSON.T): Option[Args] =
    1.12 @@ -173,7 +173,8 @@
    1.13          export_pattern <- JSON.string_default(json, "export_pattern")
    1.14          check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
    1.15          check_limit <- JSON.int_default(json, "check_limit")
    1.16 -        watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout")
    1.17 +        watchdog_timeout <-
    1.18 +          JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
    1.19          nodes_status_delay <-
    1.20            JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    1.21        }