--- 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>\<open>-T\<close> 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>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
+ \<^verbatim>\<open>rsync\<close>.
\<close>
subsubsection \<open>Examples\<close>
--- 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)
}
--- 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)
}
)
--- 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 "") +