tuned;
authorwenzelm
Wed, 18 Dec 2019 15:31:49 +0100
changeset 71307 4a7a1da27087
parent 71306 113779776ee4
child 71308 384755399fa8
tuned;
src/Pure/General/ssh.scala
--- 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)
       }