author | wenzelm |
Tue, 13 Mar 2018 17:13:20 +0100 | |
changeset 67844 | 7f82445e8f0e |
parent 67843 | ff561f6e0a8e |
child 67845 | 46fa8c2c142a |
--- a/src/Pure/Admin/remote_dmg.scala Tue Mar 13 16:08:13 2018 +0100 +++ b/src/Pure/Admin/remote_dmg.scala Tue Mar 13 17:13:20 2018 +0100 @@ -56,7 +56,7 @@ case _ => getopts.usage() } - val options = Options.init + val options = Options.init() using(SSH.open_session(options, host = host, user = user, port = port))( remote_dmg(_, tar_gz_file, dmg_file, volume_name)) }