diff -r 6dd1460f6920 -r ea804c814693 src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Sat Sep 08 13:22:23 2018 +0200 +++ b/src/Doc/System/Server.thy Sat Sep 08 13:36:40 2018 +0200 @@ -909,7 +909,7 @@ \quad~~\export_pattern?: string,\ \\ \quad~~\check_delay?: double,\ & \<^bold>\default:\ \<^verbatim>\0.5\ \\ \quad~~\check_limit?: int,\ \\ - \quad~~\watchdog_timeout?: double,\ \\ + \quad~~\watchdog_timeout?: double,\ & \<^bold>\default:\ \<^verbatim>\600.0\ \\ \quad~~\nodes_status_delay?: double}\ & \<^bold>\default:\ \<^verbatim>\-1.0\ \\ \end{tabular}