# HG changeset patch # User wenzelm # Date 1663325344 -7200 # Node ID e517a38dc0e6f8f2035b8f51ebf6e6b0f94d4972 # Parent dbafa8d688fbe403771ea9d03a8780ffa736ad43 clarified options; diff -r dbafa8d688fb -r e517a38dc0e6 etc/options --- a/etc/options Thu Sep 15 21:37:17 2022 +0200 +++ b/etc/options Fri Sep 16 12:49:04 2022 +0200 @@ -296,10 +296,10 @@ -- "enable SSH compression" option ssh_alive_interval : real = 30 - -- "time interval to keep SSH server connection alive (seconds)" + -- "time interval to keep SSH server connection alive (seconds, ignore value < 0)" option ssh_alive_count_max : int = 3 - -- "maximum number of messages to keep SSH server connection alive" + -- "maximum number of messages to keep SSH server connection alive (ignore value < 0)" section "Phabricator" diff -r dbafa8d688fb -r e517a38dc0e6 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Thu Sep 15 21:37:17 2022 +0200 +++ b/src/Pure/General/ssh.scala Fri Sep 16 12:49:04 2022 +0200 @@ -44,10 +44,13 @@ control_master: Boolean = false, control_path: String = "" ): List[String] = { - List("BatchMode=yes", - entry("ServerAliveInterval", options.real("ssh_alive_interval").round), - entry("ServerAliveCountMax", options.int("ssh_alive_count_max")), - entry("Compression", options.bool("ssh_compression"))) ::: + val ssh_compression = options.bool("ssh_compression") + val ssh_alive_interval = options.real("ssh_alive_interval").round + val ssh_alive_count_max = options.int("ssh_alive_count_max") + + List("BatchMode=yes", entry("Compression", ssh_compression)) ::: + (if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) ::: + (if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) ::: (if (port > 0) List(entry("Port", port)) else Nil) ::: (if (user.nonEmpty) List(entry("User", user)) else Nil) ::: (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::