diff -r aab9bb081f01 -r a3c694039fd6 src/Pure/General/mercurial.scala --- 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))