# HG changeset patch
# User wenzelm
# Date 1476088864 -7200
# Node ID 14782d58a5038e9e41b737b2e5ba820124a28d34
# Parent  42bcd207598d94b13f2fa1ede8f5bd8e9030cd59
more generous timeout default (see also jEdit/FTP);

diff -r 42bcd207598d -r 14782d58a503 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 10:33:52 2016 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 10 10:41:04 2016 +0200
@@ -93,6 +93,7 @@
 class SSH private(val jsch: JSch)
 {
   def open_session(host: String, port: Int = 22, user: String = null,
+    connect_timeout: Time = Time.seconds(60),
     compression: Boolean = true): SSH.Session =
   {
     val session = jsch.getSession(user, host, port)
@@ -106,7 +107,9 @@
       session.setConfig("compression_level", "9")
     }
 
-    session.connect
+    if (connect_timeout.is_zero) session.connect
+    else session.connect(connect_timeout.ms.toInt)
+
     new SSH.Session(session)
   }
 }