src/Doc/System/Server.thy
changeset 68947 ea804c814693
parent 68908 abc338d25640
child 68957 eef4e983fd9d
     1.1 --- a/src/Doc/System/Server.thy	Sat Sep 08 13:22:23 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Sat Sep 08 13:36:40 2018 +0200
     1.3 @@ -909,7 +909,7 @@
     1.4    \quad~~\<open>export_pattern?: string,\<close> \\
     1.5    \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
     1.6    \quad~~\<open>check_limit?: int,\<close> \\
     1.7 -  \quad~~\<open>watchdog_timeout?: double,\<close> \\
     1.8 +  \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
     1.9    \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
    1.10    \end{tabular}
    1.11