# HG changeset patch # User wenzelm # Date 1663058687 -7200 # Node ID a144603170b40424e6c7b467f5f99ea97282aad1 # Parent c6e0a51f2a93d9f9c32d975594796d9ed63a632f clarified command-line; diff -r c6e0a51f2a93 -r a144603170b4 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Tue Sep 13 10:34:52 2022 +0200 +++ b/src/Doc/System/Misc.thy Tue Sep 13 10:44:47 2022 +0200 @@ -312,10 +312,9 @@ Options are: -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) + -P protect spaces in target file names: more robust, less portable -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) @@ -356,7 +355,7 @@ \<^medskip> Option \<^verbatim>\-p\ specifies an explicit port for the SSH connection underlying \<^verbatim>\rsync\; the default is taken from the user's \<^path>\ssh_config\ file. - \<^medskip> Option \<^verbatim>\-S\ uses \<^verbatim>\rsync --protect-args\ to work robustly with spaces or + \<^medskip> Option \<^verbatim>\-P\ uses \<^verbatim>\rsync --protect-args\ to work robustly with spaces or special characters of the shell. This requires at least \<^verbatim>\rsync 3.0.0\, which is not always available --- notably on macOS. Assuming traditional Unix-style naming of files and directories, it is safe to omit this option diff -r c6e0a51f2a93 -r a144603170b4 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue Sep 13 10:34:52 2022 +0200 +++ b/src/Doc/System/Sessions.thy Tue Sep 13 10:44:47 2022 +0200 @@ -931,8 +931,7 @@ -I NAME include session heap image and build database (based on accidental local state) -J preserve *.jar files - -S robust (but less portable) treatment of spaces in - file and directory names on the target + -P protect spaces in target file names: more robust, less portable -T thorough treatment of file content and directory times -a REV explicit AFP revision (default: state of working directory) -n no changes: dry-run @@ -951,7 +950,7 @@ sub-directory with the literal name \<^verbatim>\AFP\; thus it can be easily included elsewhere, e.g. @{tool build}~\<^verbatim>\-d\~\<^verbatim>\'~~/AFP'\ on the remote side. - \<^medskip> Options \<^verbatim>\-S\, \<^verbatim>\-T\, \<^verbatim>\-n\, \<^verbatim>\-p\, \<^verbatim>\-v\ are the same as the underlying + \<^medskip> Options \<^verbatim>\-P\, \<^verbatim>\-T\, \<^verbatim>\-n\, \<^verbatim>\-p\, \<^verbatim>\-v\ are the same as the underlying @{tool hg_sync}. \<^medskip> Options \<^verbatim>\-r\ and \<^verbatim>\-a\ are the same as option \<^verbatim>\-r\ for @{tool hg_sync},