author | wenzelm |
Wed, 18 Dec 2019 15:31:49 +0100 | |
changeset 71307 | 4a7a1da27087 |
parent 71306 | 113779776ee4 |
child 71308 | 384755399fa8 |
--- a/src/Pure/General/ssh.scala Wed Dec 18 15:10:50 2019 +0100 +++ b/src/Pure/General/ssh.scala Wed Dec 18 15:31:49 2019 +0100 @@ -21,11 +21,11 @@ object Target { - val Pattern = "^([^@]+)@(.+)$".r + val User_Host = "^([^@]+)@(.+)$".r def parse(s: String): (String, String) = s match { - case Pattern(user, host) => (user, host) + case User_Host(user, host) => (user, host) case _ => ("", s) }