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