# 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>\<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> uses \<^verbatim>\<open>rsync --protect-args\<close> to work robustly with spaces or
+  \<^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
   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>\<open>AFP\<close>; thus it can be easily included
   elsewhere, e.g. @{tool build}~\<^verbatim>\<open>-d\<close>~\<^verbatim>\<open>'~~/AFP'\<close> on the remote side.
 
-  \<^medskip> Options \<^verbatim>\<open>-S\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying
+  \<^medskip> Options \<^verbatim>\<open>-P\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying
   @{tool hg_sync}.
 
   \<^medskip> Options \<^verbatim>\<open>-r\<close> and \<^verbatim>\<open>-a\<close> are the same as option \<^verbatim>\<open>-r\<close> for @{tool hg_sync},