src/Pure/General/ssh.scala
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)