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