--- a/src/Doc/System/Misc.thy Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Doc/System/Misc.thy Tue Sep 13 11:56:38 2022 +0200
@@ -315,10 +315,11 @@
-P protect spaces in target file names: more robust, less portable
-R ROOT explicit repository root directory
(default: implicit from current directory)
+ -S PATH SSH control path for connection multiplexing
-T thorough treatment of file content and directory times
-n no changes: dry-run
+ -p PORT SSH port
-r REV explicit revision (default: state of working directory)
- -p PORT explicit SSH port
-v verbose
Synchronize Mercurial repository with TARGET directory,
@@ -355,6 +356,9 @@
\<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
\<^verbatim>\<open>rsync\<close>; the default is taken from the user's \<^path>\<open>ssh_config\<close> file.
+ \<^medskip> Option \<^verbatim>\<open>-S\<close> specifies the control path (Unix socket) to an existing SSH
+ connection that supports multiplexing (\<^verbatim>\<open>ssh -M -S\<close>~\<open>socket\<close>).
+
\<^medskip> Option \<^verbatim>\<open>-P\<close> uses \<^verbatim>\<open>rsync --protect-args\<close> to work robustly with spaces or
special characters of the shell. This requires at least \<^verbatim>\<open>rsync 3.0.0\<close>,
which is not always available --- notably on macOS. Assuming traditional