more generous timeout default (see also jEdit/FTP);
authorwenzelm
Mon, 10 Oct 2016 10:41:04 +0200
changeset 64127 14782d58a503
parent 64126 42bcd207598d
child 64128 cc5ea4d648d8
more generous timeout default (see also jEdit/FTP);
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)
   }
 }