tuned signature;
authorwenzelm
Mon, 13 Nov 2017 14:39:03 +0100
changeset 67067 02729ced9b1e
parent 67066 1645cef7a49c
child 67068 46ce32fd5f53
tuned signature;
src/Pure/Admin/build_log.scala
src/Pure/Admin/remote_dmg.scala
src/Pure/General/ssh.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)
     }
 
--- 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)
--- 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)