diff -r a144603170b4 -r 1bb677cceea4 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue Sep 13 10:44:47 2022 +0200 +++ b/src/Doc/System/Sessions.thy Tue Sep 13 11:56:38 2022 +0200 @@ -932,11 +932,12 @@ (based on accidental local state) -J preserve *.jar files -P protect spaces in target file names: more robust, less portable + -S PATH SSH control path for connection multiplexing -T thorough treatment of file content and directory times -a REV explicit AFP revision (default: state of working directory) -n no changes: dry-run + -p PORT SSH port -r REV explicit revision (default: state of working directory) - -p PORT explicit SSH port -v verbose Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\} @@ -950,8 +951,8 @@ 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>\-P\, \<^verbatim>\-T\, \<^verbatim>\-n\, \<^verbatim>\-p\, \<^verbatim>\-v\ are the same as the underlying - @{tool hg_sync}. + \<^medskip> Options \<^verbatim>\-P\, \<^verbatim>\-S\, \<^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}, but for the Isabelle and AFP repositories, respectively. The AFP version is