src/Pure/General/ssh.scala
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)
       }