src/Pure/General/mercurial.scala
changeset 76169 a3c694039fd6
parent 76136 1bb677cceea4
child 76540 83de6e9ae983
--- a/src/Pure/General/mercurial.scala	Fri Sep 16 14:02:02 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Fri Sep 16 14:26:42 2022 +0200
@@ -467,40 +467,38 @@
 
     /* remote repository */
 
-    val remote_url =
-      remote match {
-        case _ if remote.startsWith("ssh://") =>
-          val ssh_url = remote + "/" + repos_name
+    val remote_url = {
+      if (remote.startsWith("ssh://")) {
+        val ssh_url = remote + "/" + repos_name
+
+        if (!remote_exists) {
+          try { local_hg.command("init", ssh_url, repository = false).check }
+          catch { case ERROR(msg) => progress.echo_warning(msg) }
+        }
 
-          if (!remote_exists) {
-            try { local_hg.command("init", ssh_url, repository = false).check }
-            catch { case ERROR(msg) => progress.echo_warning(msg) }
+        ssh_url
+      }
+      else {
+        val phabricator = Phabricator.API(remote)
+
+        var repos =
+          phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
+            if (remote_exists) {
+              error("Remote repository " +
+                quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
+            }
+            else phabricator.create_repository(repos_name, short_name = repos_name)
           }
 
-          ssh_url
-
-        case SSH.Target(user, host) =>
-          val phabricator = Phabricator.API(user, host)
+        while (repos.importing) {
+          progress.echo("Awaiting remote repository ...")
+          Time.seconds(0.5).sleep()
+          repos = phabricator.the_repository(repos.phid)
+        }
 
-          var repos =
-            phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
-              if (remote_exists) {
-                error("Remote repository " +
-                  quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
-              }
-              else phabricator.create_repository(repos_name, short_name = repos_name)
-            }
-
-          while (repos.importing) {
-            progress.echo("Awaiting remote repository ...")
-            Time.seconds(0.5).sleep()
-            repos = phabricator.the_repository(repos.phid)
-          }
-
-          repos.ssh_url
-
-        case _ => error("Malformed remote specification " + quote(remote))
+        repos.ssh_url
       }
+    }
 
     progress.echo("Remote repository " + quote(remote_url))