# HG changeset patch
# User wenzelm
# Date 1476351820 -7200
# Node ID f4d5eb78b8a5b1f07daa0d3050ed2b3d424bcc1a
# Parent  68e95e5b2b7d178006e4336c1674aa2290a8a506
tuned;

diff -r 68e95e5b2b7d -r f4d5eb78b8a5 src/Pure/Admin/remote_dmg.scala
--- 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()
           }
diff -r 68e95e5b2b7d -r f4d5eb78b8a5 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Oct 13 11:22:27 2016 +0200
+++ b/src/Pure/General/ssh.scala	Thu Oct 13 11:43:40 2016 +0200
@@ -17,9 +17,9 @@
 
 object SSH
 {
-  /* user@host syntax */
+  /* target machine: user@host syntax */
 
-  object User_Host
+  object Target
   {
     val Pattern = "^([^@]+)@(.+)$".r
 
@@ -30,10 +30,10 @@
       }
 
     def unapplySeq(s: String): Option[List[String]] =
-    {
-      val (user, host) = parse(s)
-      Some(List(user, host))
-    }
+      parse(s) match {
+        case (_, "") => None
+        case (user, host) => Some(List(user, host))
+      }
   }
 
   val default_port = 22