# HG changeset patch
# User wenzelm
# Date 1510580343 -3600
# Node ID 02729ced9b1eae158b6a559e597da1a853ab1a70
# Parent  1645cef7a49c6019d0534974326f4e7bac400af8
tuned signature;

diff -r 1645cef7a49c -r 02729ced9b1e src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Nov 13 14:31:25 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Nov 13 14:39:03 2017 +0100
@@ -892,7 +892,7 @@
         user = user, password = password, database = database, host = host, port = port,
         ssh =
           if (ssh_host == "") None
-          else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)),
+          else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = port)),
         ssh_close = true)
     }
 
diff -r 1645cef7a49c -r 02729ced9b1e src/Pure/Admin/remote_dmg.scala
--- a/src/Pure/Admin/remote_dmg.scala	Mon Nov 13 14:31:25 2017 +0100
+++ b/src/Pure/Admin/remote_dmg.scala	Mon Nov 13 14:39:03 2017 +0100
@@ -56,8 +56,8 @@
             case _ => getopts.usage()
           }
 
-        val ssh = SSH.init_context(Options.init)
-        using(ssh.open_session(user = user, host = host, port = port))(
+        val options = Options.init
+        using(SSH.open_session(options, host = host, user = user, port = port))(
           remote_dmg(_, tar_gz_file, dmg_file, volume_name))
       }
     }, admin = true)
diff -r 1645cef7a49c -r 02729ced9b1e src/Pure/General/ssh.scala
--- 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)