| changeset 71307 | 4a7a1da27087 |
| parent 69427 | ff2f39a221d4 |
| child 71358 | ec48da635e6c |
--- 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) }