changeset 64185 | f4d5eb78b8a5 |
parent 64161 | 2b1128e95dfb |
child 64233 | ef6f7e8a018c |
--- a/src/Pure/Admin/remote_dmg.scala Thu Oct 13 11:22:27 2016 +0200 +++ b/src/Pure/Admin/remote_dmg.scala Thu Oct 13 11:43:40 2016 +0200 @@ -52,7 +52,7 @@ val more_args = getopts(args) val (user, host, tar_gz_file, dmg_file) = more_args match { - case List(SSH.User_Host(user, host), tar_gz_file, dmg_file) => + case List(SSH.Target(user, host), tar_gz_file, dmg_file) => (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file)) case _ => getopts.usage() }