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) :::