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