--- 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()
}
--- 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