changeset 67067 | 02729ced9b1e |
parent 67066 | 1645cef7a49c |
child 67273 | c573cfb2c407 |
--- a/src/Pure/General/ssh.scala Mon Nov 13 14:31:25 2017 +0100 +++ b/src/Pure/General/ssh.scala Mon Nov 13 14:39:03 2017 +0100 @@ -70,6 +70,9 @@ new Context(options, jsch) } + def open_session(options: Options, host: String, user: String = "", port: Int = 0): Session = + init_context(options).open_session(host = host, user = user, port = port) + class Context private[SSH](val options: Options, val jsch: JSch) { def update_options(new_options: Options): Context = new Context(new_options, jsch)