# HG changeset patch
# User wenzelm
# Date 1663270637 -7200
# Node ID dbafa8d688fbe403771ea9d03a8780ffa736ad43
# Parent  cf469736000c8aae29d965457599ee5dff7dcc33
discontinued unclear timeout (stemming from jEdit JSch setup, see 14782d58a503), to make it work with native Windows ssh.exe;

diff -r cf469736000c -r dbafa8d688fb etc/options
--- a/etc/options	Thu Sep 15 21:33:46 2022 +0200
+++ b/etc/options	Thu Sep 15 21:37:17 2022 +0200
@@ -295,9 +295,6 @@
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
-option ssh_connect_timeout : real = 60
-  -- "SSH connection timeout (seconds)"
-
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
diff -r cf469736000c -r dbafa8d688fb src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Sep 15 21:33:46 2022 +0200
+++ b/src/Pure/General/ssh.scala	Thu Sep 15 21:37:17 2022 +0200
@@ -45,7 +45,6 @@
       control_path: String = ""
     ): List[String] = {
       List("BatchMode=yes",
-        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"))) :::