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