# HG changeset patch # User wenzelm # Date 1653995686 -7200 # Node ID c635368021b6bc0904431357077b8ea3951f9158 # Parent 108b8985a2d9f4f9ccec1628997c366e9c55cea6 support explicit SSH port; diff -r 108b8985a2d9 -r c635368021b6 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Tue May 31 12:48:12 2022 +0200 +++ b/src/Doc/System/Misc.thy Tue May 31 13:14:46 2022 +0200 @@ -320,6 +320,7 @@ -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) + -p PORT explicit SSH port (default: 22) -v verbose Synchronize Mercurial repository with TARGET directory, @@ -352,6 +353,9 @@ \<^medskip> Option \<^verbatim>\-T\ indicates thorough treatment of file content and directory times. The default is to consider files with equal time and size already as equal, and to ignore time stamps on directories. + + \<^medskip> Option \<^verbatim>\-p\ specifies an explicit port for the SSH connection underlying + \<^verbatim>\rsync\. \ subsubsection \Examples\ diff -r 108b8985a2d9 -r c635368021b6 src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala Tue May 31 12:48:12 2022 +0200 +++ b/src/Pure/Admin/sync_repos.scala Tue May 31 13:14:46 2022 +0200 @@ -10,6 +10,7 @@ object Sync_Repos { def sync_repos(target: String, progress: Progress = new Progress, + port: Int = SSH.default_port, verbose: Boolean = false, thorough: Boolean = false, preserve_jars: Boolean = false, @@ -27,8 +28,8 @@ val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit = - hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough, - dry_run = dry_run, clean = clean, filter = filter ::: more_filter) + hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose, + thorough = thorough, dry_run = dry_run, clean = clean, filter = filter ::: more_filter) progress.echo("\n* Isabelle repository:") sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID")) @@ -37,7 +38,7 @@ Isabelle_System.with_tmp_dir("sync") { tmp_dir => val id_path = tmp_dir + Path.explode("ISABELLE_ID") File.write(id_path, isabelle_hg.id(rev = rev)) - Isabelle_System.rsync(thorough = thorough, + Isabelle_System.rsync(port = port, thorough = thorough, args = List(File.standard_path(id_path), target_dir + "etc/")) } } @@ -58,6 +59,7 @@ var afp_rev = "" var dry_run = false var rev = "" + var port = SSH.default_port var verbose = false val getopts = Getopts(""" @@ -73,6 +75,7 @@ -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) + -p PORT explicit SSH port (default: """ + SSH.default_port + """) -v verbose Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync". @@ -95,6 +98,7 @@ "f" -> (_ => dry_run = false), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), + "p:" -> (arg => port = Value.Int.parse(arg)), "v" -> (_ => verbose = true)) val more_args = getopts(args) @@ -105,7 +109,7 @@ } val progress = new Console_Progress - sync_repos(target, progress = progress, verbose = verbose, thorough = thorough, + sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough, preserve_jars = preserve_jars, dry_run = dry_run, clean = clean, rev = rev, afp_root = afp_root, afp_rev = afp_rev) } diff -r 108b8985a2d9 -r c635368021b6 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue May 31 12:48:12 2022 +0200 +++ b/src/Pure/General/mercurial.scala Tue May 31 13:14:46 2022 +0200 @@ -253,6 +253,7 @@ def sync(target: String, progress: Progress = new Progress, + port: Int = SSH.default_port, verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, @@ -279,7 +280,7 @@ (Nil, source) } Isabelle_System.rsync( - progress = progress, verbose = verbose, thorough = thorough, + progress = progress, port = port, verbose = verbose, thorough = thorough, dry_run = dry_run, clean = clean, filter = filter, args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)) } @@ -491,6 +492,7 @@ var thorough = false var dry_run = false var rev = "" + var port = SSH.default_port var verbose = false val getopts = Getopts(""" @@ -506,6 +508,7 @@ -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) + -p PORT explicit SSH port (default: """ + SSH.default_port + """) -v verbose Synchronize Mercurial repository with TARGET directory, @@ -518,6 +521,7 @@ "f" -> (_ => dry_run = false), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), + "p:" -> (arg => port = Value.Int.parse(arg)), "v" -> (_ => verbose = true)) val more_args = getopts(args) @@ -533,7 +537,7 @@ case Some(dir) => repository(dir) case None => the_repository(Path.current) } - hg.sync(target, progress = progress, verbose = verbose, thorough = thorough, + hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough, dry_run = dry_run, clean = clean, filter = filter, rev = rev) } ) diff -r 108b8985a2d9 -r c635368021b6 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue May 31 12:48:12 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Tue May 31 13:14:46 2022 +0200 @@ -423,6 +423,7 @@ def rsync( cwd: JFile = null, progress: Progress = new Progress, + port: Int = SSH.default_port, verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, @@ -431,7 +432,7 @@ args: List[String] = Nil ): Unit = { val script = - "rsync --protect-args --archive" + + "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + (if (verbose || dry_run) " --verbose" else "") + (if (thorough) " --ignore-times" else " --omit-dir-times") + (if (dry_run) " --dry-run" else "") +