# HG changeset patch
# User wenzelm
# Date 1663270426 -7200
# Node ID cf469736000c8aae29d965457599ee5dff7dcc33
# Parent  5e8bc80df6b323e51b206d817575c5f7d68e8c96
proper time values in seconds;

diff -r 5e8bc80df6b3 -r cf469736000c src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Sep 15 14:03:17 2022 +0200
+++ b/src/Pure/General/ssh.scala	Thu Sep 15 21:33:46 2022 +0200
@@ -35,6 +35,7 @@
   object Config {
     def entry(x: String, y: String): String = x + "=" + y
     def entry(x: String, y: Int): String = entry(x, y.toString)
+    def entry(x: String, y: Long): String = entry(x, y.toString)
     def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no")
 
     def make(options: Options,
@@ -44,8 +45,8 @@
       control_path: String = ""
     ): List[String] = {
       List("BatchMode=yes",
-        entry("ConnectTimeout", options.seconds("ssh_connect_timeout").ms.toInt),
-        entry("ServerAliveInterval", options.seconds("ssh_alive_interval").ms.toInt),
+        entry("ConnectTimeout", options.real("ssh_connect_timeout").round),
+        entry("ServerAliveInterval", options.real("ssh_alive_interval").round),
         entry("ServerAliveCountMax", options.int("ssh_alive_count_max")),
         entry("Compression", options.bool("ssh_compression"))) :::
       (if (port > 0) List(entry("Port", port)) else Nil) :::
@@ -57,6 +58,7 @@
     def option(entry: String): String = "-o " + Bash.string(entry)
     def option(x: String, y: String): String = option(entry(x, y))
     def option(x: String, y: Int): String = option(entry(x, y))
+    def option(x: String, y: Long): String = option(entry(x, y))
     def option(x: String, y: Boolean): String = option(entry(x, y))
 
     def command(command: String, config: List[String]): String =