# HG changeset patch # User wenzelm # Date 1663055948 -7200 # Node ID 8b695e59db3fefd89d3bee0c7b17c43d2e44104d # Parent b703cecf9bd04e27056fecc08fc8ab7acf9d50c8 clarified default: do not override port from ssh_config, which could be different from 22; diff -r b703cecf9bd0 -r 8b695e59db3f src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Tue Sep 13 09:45:02 2022 +0200 +++ b/src/Doc/System/Misc.thy Tue Sep 13 09:59:08 2022 +0200 @@ -319,7 +319,7 @@ -T thorough treatment of file content and directory times -n no changes: dry-run -r REV explicit revision (default: state of working directory) - -p PORT explicit SSH port (default: 22) + -p PORT explicit SSH port -v verbose Synchronize Mercurial repository with TARGET directory, @@ -354,7 +354,7 @@ equal, and to ignore time stamps on directories. \<^medskip> Option \<^verbatim>\-p\ specifies an explicit port for the SSH connection underlying - \<^verbatim>\rsync\. + \<^verbatim>\rsync\; the default is taken from the user's \<^path>\ssh_config\ file. \<^medskip> Option \<^verbatim>\-S\ uses \<^verbatim>\rsync --protect-args\ to work robustly with spaces or special characters of the shell. This requires at least \<^verbatim>\rsync 3.0.0\, diff -r b703cecf9bd0 -r 8b695e59db3f src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue Sep 13 09:45:02 2022 +0200 +++ b/src/Doc/System/Sessions.thy Tue Sep 13 09:59:08 2022 +0200 @@ -937,7 +937,7 @@ -a REV explicit AFP revision (default: state of working directory) -n no changes: dry-run -r REV explicit revision (default: state of working directory) - -p PORT explicit SSH port (default: 22) + -p PORT explicit SSH port -v verbose Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\} diff -r b703cecf9bd0 -r 8b695e59db3f src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue Sep 13 09:45:02 2022 +0200 +++ b/src/Pure/General/mercurial.scala Tue Sep 13 09:59:08 2022 +0200 @@ -566,7 +566,7 @@ var thorough = false var dry_run = false var rev = "" - var port = SSH.default_port + var port = 0 var verbose = false val getopts = Getopts(""" @@ -582,7 +582,7 @@ -T thorough treatment of file content and directory times -n no changes: dry-run -r REV explicit revision (default: state of working directory) - -p PORT explicit SSH port (default: """ + SSH.default_port + """) + -p PORT explicit SSH port -v verbose Synchronize Mercurial repository with TARGET directory, diff -r b703cecf9bd0 -r 8b695e59db3f src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Tue Sep 13 09:45:02 2022 +0200 +++ b/src/Pure/General/rsync.scala Tue Sep 13 09:59:08 2022 +0200 @@ -9,12 +9,12 @@ object Rsync { sealed case class Context(progress: Progress, - port: Int = SSH.default_port, + port: Int = 0, archive: Boolean = true, protect_args: Boolean = true // requires rsync 3.0.0, or later ) { def command: String = - "rsync --rsh=" + Bash.string("ssh -p " + port) + + "rsync --rsh=" + Bash.string("ssh" + (if (port > 0) "-p " + port else "")) + (if (archive) " --archive" else "") + (if (protect_args) " --protect-args" else "") } diff -r b703cecf9bd0 -r 8b695e59db3f src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Tue Sep 13 09:45:02 2022 +0200 +++ b/src/Pure/General/ssh.scala Tue Sep 13 09:59:08 2022 +0200 @@ -28,17 +28,9 @@ } } - val default_port = 22 - def make_port(port: Int): Int = if (port > 0) port else default_port - - def port_suffix(port: Int): String = - if (port == default_port) "" else ":" + port + def port_suffix(port: Int): String = if (port > 0) ":" + port else "" - def user_prefix(user: String): String = - proper_string(user) match { - case None => "" - case Some(name) => name + "@" - } + def user_prefix(user: String): String = if (user.nonEmpty) user + "@" else "" /* OpenSSH configuration and command-line */ @@ -50,7 +42,7 @@ def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no") def make(options: Options, - port: Int = default_port, + port: Int = 0, user: String = "", control_master: Boolean = false, control_path: String = "" @@ -60,7 +52,7 @@ entry("ServerAliveInterval", options.seconds("ssh_alive_interval").ms.toInt), entry("ServerAliveCountMax", options.int("ssh_alive_count_max")), entry("Compression", options.bool("ssh_compression"))) ::: - (if (port > 0 && port != default_port) List(entry("Port", port)) else Nil) ::: + (if (port > 0) List(entry("Port", port)) else Nil) ::: (if (user.nonEmpty) List(entry("User", user)) else Nil) ::: (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) ::: (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil) @@ -101,7 +93,7 @@ } else (false, "") - new Session(options, host, make_port(port), user, control_master, control_path) + new Session(options, host, port, user, control_master, control_path) } class Session private[SSH]( diff -r b703cecf9bd0 -r 8b695e59db3f src/Pure/Tools/sync.scala --- a/src/Pure/Tools/sync.scala Tue Sep 13 09:45:02 2022 +0200 +++ b/src/Pure/Tools/sync.scala Tue Sep 13 09:59:08 2022 +0200 @@ -89,7 +89,7 @@ var afp_rev = "" var dry_run = false var rev = "" - var port = SSH.default_port + var port = 0 var verbose = false val getopts = Getopts(""" @@ -107,7 +107,7 @@ -a REV explicit AFP revision (default: state of working directory) -n no changes: dry-run -r REV explicit revision (default: state of working directory) - -p PORT explicit SSH port (default: """ + SSH.default_port + """) + -p PORT explicit SSH port -v verbose Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".