changeset 64257 | 9d51ac055cec |
parent 64256 | c3197aeae90b |
child 64304 | 96bc94c87a81 |
--- a/src/Pure/Admin/remote_dmg.scala Sun Oct 16 17:44:37 2016 +0200 +++ b/src/Pure/Admin/remote_dmg.scala Sun Oct 16 17:50:40 2016 +0200 @@ -56,7 +56,7 @@ case _ => getopts.usage() } - val ssh = SSH.init(Options.init) + val ssh = SSH.init_context(Options.init) using(ssh.open_session(user = user, host = host, port = port))( remote_dmg(_, tar_gz_file, dmg_file, volume_name)) }