--- a/src/Pure/General/rsync.scala Fri Sep 16 14:26:42 2022 +0200
+++ b/src/Pure/General/rsync.scala Fri Sep 16 14:57:48 2022 +0200
@@ -14,14 +14,8 @@
archive: Boolean = true,
protect_args: Boolean = true // requires rsync 3.0.0, or later
) {
- require(ssh_control_path.isEmpty || ssh_control_path == Bash.string(ssh_control_path),
- "Malformed socket path: " + quote(ssh_control_path))
-
def command: String = {
- val ssh_command =
- "ssh" + (if (ssh_port > 0) " -p " + ssh_port else "") +
- (if (ssh_control_path.nonEmpty) " -o ControlPath=" + ssh_control_path else "")
-
+ val ssh_command = SSH.client_command(port = ssh_port, control_path = ssh_control_path)
"rsync --rsh=" + Bash.string(ssh_command) +
(if (archive) " --archive" else "") +
(if (protect_args) " --protect-args" else "")
--- a/src/Pure/General/ssh.scala Fri Sep 16 14:26:42 2022 +0200
+++ b/src/Pure/General/ssh.scala Fri Sep 16 14:57:48 2022 +0200
@@ -13,6 +13,17 @@
object SSH {
+ /* client command */
+
+ def client_command(port: Int = 0, control_path: String = ""): String =
+ if (control_path.isEmpty || control_path == Bash.string(control_path)) {
+ "ssh" +
+ (if (port > 0) " -p " + port else "") +
+ (if (control_path.nonEmpty) " -o ControlPath=" + control_path else "")
+ }
+ else error ("Malformed SSH control socket: " + quote(control_path))
+
+
/* OpenSSH configuration and command-line */
// see https://linux.die.net/man/5/ssh_config
--- a/src/Pure/Tools/phabricator.scala Fri Sep 16 14:26:42 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala Fri Sep 16 14:57:48 2022 +0200
@@ -896,10 +896,8 @@
final class API private(ssh_target: String, ssh_port: Int) {
/* connection */
- require(ssh_target.nonEmpty && ssh_port >= 0, "bad ssh host or port")
-
private def ssh_port_suffix: String =
- if (ssh_port != default_system_port) ":" + ssh_port else ""
+ if (ssh_port > 0) ":" + ssh_port else ""
override def toString: String = ssh_target + ssh_port_suffix
def hg_url: String = "ssh://" + ssh_target + ssh_port_suffix