tuned signature;
authorwenzelm
Mon Nov 13 14:39:03 2017 +0100 (3 months ago)
changeset 6706702729ced9b1e
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
     1.1 --- a/src/Pure/Admin/build_log.scala	Mon Nov 13 14:31:25 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Mon Nov 13 14:39:03 2017 +0100
     1.3 @@ -892,7 +892,7 @@
     1.4          user = user, password = password, database = database, host = host, port = port,
     1.5          ssh =
     1.6            if (ssh_host == "") None
     1.7 -          else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)),
     1.8 +          else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = port)),
     1.9          ssh_close = true)
    1.10      }
    1.11  
     2.1 --- a/src/Pure/Admin/remote_dmg.scala	Mon Nov 13 14:31:25 2017 +0100
     2.2 +++ b/src/Pure/Admin/remote_dmg.scala	Mon Nov 13 14:39:03 2017 +0100
     2.3 @@ -56,8 +56,8 @@
     2.4              case _ => getopts.usage()
     2.5            }
     2.6  
     2.7 -        val ssh = SSH.init_context(Options.init)
     2.8 -        using(ssh.open_session(user = user, host = host, port = port))(
     2.9 +        val options = Options.init
    2.10 +        using(SSH.open_session(options, host = host, user = user, port = port))(
    2.11            remote_dmg(_, tar_gz_file, dmg_file, volume_name))
    2.12        }
    2.13      }, admin = true)
     3.1 --- a/src/Pure/General/ssh.scala	Mon Nov 13 14:31:25 2017 +0100
     3.2 +++ b/src/Pure/General/ssh.scala	Mon Nov 13 14:39:03 2017 +0100
     3.3 @@ -70,6 +70,9 @@
     3.4      new Context(options, jsch)
     3.5    }
     3.6  
     3.7 +  def open_session(options: Options, host: String, user: String = "", port: Int = 0): Session =
     3.8 +    init_context(options).open_session(host = host, user = user, port = port)
     3.9 +
    3.10    class Context private[SSH](val options: Options, val jsch: JSch)
    3.11    {
    3.12      def update_options(new_options: Options): Context = new Context(new_options, jsch)