etc/options
changeset 67273 c573cfb2c407
parent 67194 1c0a6a957114
child 67395 b39d596b77ce
--- a/etc/options	Sat Dec 23 23:07:26 2017 +0100
+++ b/etc/options	Sun Dec 24 12:48:43 2017 +0100
@@ -238,6 +238,9 @@
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
+option ssh_alive_count_max : int = 3
+  -- "maximum number of messages to keep SSH server connection alive"
+
 
 section "Build Log Database"