--- a/src/Doc/System/Sessions.thy Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Doc/System/Sessions.thy Sat Apr 08 19:32:09 2023 +0200
@@ -936,7 +936,6 @@
-I NAME include session heap image and build database
(based on accidental local state)
-J preserve *.jar files
- -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)
-s HOST SSH host name for remote target (default: local)
@@ -957,7 +956,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>-P\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-s\<close>, \<^verbatim>\<open>-u\<close>, \<^verbatim>\<open>-v\<close> are the same as
+ \<^medskip> Options \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-s\<close>, \<^verbatim>\<open>-u\<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},