clarified options;
authorwenzelm
Fri, 16 Sep 2022 12:49:04 +0200
changeset 76167 e517a38dc0e6
parent 76166 dbafa8d688fb
child 76168 aab9bb081f01
clarified options;
etc/options
src/Pure/General/ssh.scala
--- 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"
--- 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) :::