--- 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)