diff -r f5e96a4039a7 -r 5979f73b9db1 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Tue Sep 13 09:24:31 2022 +0200 +++ b/src/Pure/Tools/phabricator.scala Tue Sep 13 09:38:02 2022 +0200 @@ -64,7 +64,7 @@ val default_mailers: Path = Path.explode("mailers.json") - val default_system_port: Int = SSH.default_port + val default_system_port: Int = 22 val alternative_system_port = 222 val default_server_port = 2222 @@ -663,14 +663,14 @@ private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = - if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port + if (port == default_system_port) "#Port " + default_system_port else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) - case No_Port() => Some(SSH.default_port) + case No_Port() => Some(default_system_port) case _ => None }) ports match { @@ -774,7 +774,7 @@ for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) - if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port") + if (server_port == default_system_port) config.execute("config delete diffusion.ssh-port") } } @@ -889,7 +889,7 @@ /* context for operations */ - def apply(user: String, host: String, port: Int = SSH.default_port): API = + def apply(user: String, host: String, port: Int = default_system_port): API = new API(user, host, port) } @@ -898,8 +898,11 @@ require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port") - private def ssh_user_prefix: String = SSH.user_prefix(ssh_user) - private def ssh_port_suffix: String = SSH.port_suffix(ssh_port) + private def ssh_user_prefix: String = + if (ssh_user.nonEmpty) ssh_user + "@" else "" + + private def ssh_port_suffix: String = + if (ssh_port != default_system_port) ":" + ssh_port else "" override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix