equal
deleted
inserted
replaced
907 \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\ |
907 \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\ |
908 \quad~~\<open>unicode_symbols?: bool,\<close> \\ |
908 \quad~~\<open>unicode_symbols?: bool,\<close> \\ |
909 \quad~~\<open>export_pattern?: string,\<close> \\ |
909 \quad~~\<open>export_pattern?: string,\<close> \\ |
910 \quad~~\<open>check_delay?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\ |
910 \quad~~\<open>check_delay?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\ |
911 \quad~~\<open>check_limit?: int,\<close> \\ |
911 \quad~~\<open>check_limit?: int,\<close> \\ |
912 \quad~~\<open>watchdog_timeout?: double,\<close> \\ |
912 \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\ |
913 \quad~~\<open>nodes_status_delay?: double}\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\ |
913 \quad~~\<open>nodes_status_delay?: double}\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\ |
914 \end{tabular} |
914 \end{tabular} |
915 |
915 |
916 \begin{tabular}{ll} |
916 \begin{tabular}{ll} |
917 \<^bold>\<open>type\<close> \<open>export =\<close> \\ |
917 \<^bold>\<open>type\<close> \<open>export =\<close> \\ |