src/Pure/Admin/remote_dmg.scala
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))
       }