--- a/src/Doc/System/Misc.thy Mon Jun 13 11:35:00 2022 +0200
+++ b/src/Doc/System/Misc.thy Mon Jun 13 11:48:46 2022 +0200
@@ -314,6 +314,8 @@
(e.g. "protect /foo" to avoid deletion)
-R ROOT explicit repository root directory
(default: implicit from current directory)
+ -S robust (but less portable) treatment of spaces in
+ file and directory names on the target
-T thorough treatment of file content and directory times
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
@@ -353,6 +355,12 @@
\<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
\<^verbatim>\<open>rsync\<close>.
+
+ \<^medskip> Option \<^verbatim>\<open>-S\<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
+ Unix-style naming of files and directories, it is safe to omit this option
+ for the sake of portability.
\<close>
subsubsection \<open>Examples\<close>