src/Doc/System/Misc.thy

                  (default: implicit from current directory)
     -T           thorough treatment of file content and directory times
     -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,
   which can be local or remote (using notation of rsync).\<close>}
 

   suitable \<^verbatim>\<open>.hg\<close> directory is found.
 
   \<^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>
 
 text \<open>