# HG changeset patch
# User wenzelm
# Date 1663053871 -7200
# Node ID f5e96a4039a74a33e7a9225c20d08cb959d7accc
# Parent  a2b3999c2277c0d4f3c7dbc94005f0c2e5a3d9db
tuned;

diff -r a2b3999c2277 -r f5e96a4039a7 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Sep 12 23:38:18 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 09:24:31 2022 +0200
@@ -16,19 +16,16 @@
   /* target machine: user@host syntax */
 
   object Target {
-    private val User_Host = "^([^@]+)@(.+)$".r
+    def parse(s: String): (String, String) = {
+      val i = s.indexOf('@')
+      if (i <= 0) ("", s)
+      else (s.substring(0, i), s.substring(i + 1))
+    }
 
-    def parse(s: String): (String, String) =
-      s match {
-        case User_Host(user, host) => (user, host)
-        case _ => ("", s)
-      }
-
-    def unapplySeq(s: String): Option[List[String]] =
-      parse(s) match {
-        case (_, "") => None
-        case (user, host) => Some(List(user, host))
-      }
+    def unapplySeq(s: String): Option[List[String]] = {
+      val (user, host) = parse(s)
+      if (host.isEmpty) None else Some(List(user, host))
+    }
   }
 
   val default_port = 22