src/Pure/General/ssh.scala
changeset 64127 14782d58a503
parent 64126 42bcd207598d
child 64128 cc5ea4d648d8
     1.1 --- a/src/Pure/General/ssh.scala	Mon Oct 10 10:33:52 2016 +0200
     1.2 +++ b/src/Pure/General/ssh.scala	Mon Oct 10 10:41:04 2016 +0200
     1.3 @@ -93,6 +93,7 @@
     1.4  class SSH private(val jsch: JSch)
     1.5  {
     1.6    def open_session(host: String, port: Int = 22, user: String = null,
     1.7 +    connect_timeout: Time = Time.seconds(60),
     1.8      compression: Boolean = true): SSH.Session =
     1.9    {
    1.10      val session = jsch.getSession(user, host, port)
    1.11 @@ -106,7 +107,9 @@
    1.12        session.setConfig("compression_level", "9")
    1.13      }
    1.14  
    1.15 -    session.connect
    1.16 +    if (connect_timeout.is_zero) session.connect
    1.17 +    else session.connect(connect_timeout.ms.toInt)
    1.18 +
    1.19      new SSH.Session(session)
    1.20    }
    1.21  }