src/Doc/System/Misc.thy
changeset 77792 b81b2c50fc7c
parent 77783 fb61887c069a
child 78665 b0ddfa5b9ddc
equal deleted inserted replaced
77791:3e72fab0e699 77792:b81b2c50fc7c
   318 \<open>Usage: isabelle hg_sync [OPTIONS] TARGET
   318 \<open>Usage: isabelle hg_sync [OPTIONS] TARGET
   319 
   319 
   320   Options are:
   320   Options are:
   321     -F RULE      add rsync filter RULE
   321     -F RULE      add rsync filter RULE
   322                  (e.g. "protect /foo" to avoid deletion)
   322                  (e.g. "protect /foo" to avoid deletion)
   323     -P           protect spaces in target file names: more robust, less portable
       
   324     -R ROOT      explicit repository root directory
   323     -R ROOT      explicit repository root directory
   325                  (default: implicit from current directory)
   324                  (default: implicit from current directory)
   326     -T           thorough treatment of file content and directory times
   325     -T           thorough treatment of file content and directory times
   327     -n           no changes: dry-run
   326     -n           no changes: dry-run
   328     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   327     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   366   SSH host name is given, the local file-system is used. An explicit port and
   365   SSH host name is given, the local file-system is used. An explicit port and
   367   user are only required in special situations.
   366   user are only required in special situations.
   368 
   367 
   369   \<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
   368   \<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
   370   \<^verbatim>\<open>rsync\<close>; the default is taken from the user's \<^path>\<open>ssh_config\<close> file.
   369   \<^verbatim>\<open>rsync\<close>; the default is taken from the user's \<^path>\<open>ssh_config\<close> file.
   371 
       
   372   \<^medskip> Option \<^verbatim>\<open>-P\<close> uses \<^verbatim>\<open>rsync --protect-args\<close> to work robustly with spaces or
       
   373   special characters of the shell. This requires at least \<^verbatim>\<open>rsync 3.0.0\<close>,
       
   374   which is not always available --- notably on macOS. Assuming traditional
       
   375   Unix-style naming of files and directories, it is safe to omit this option
       
   376   for the sake of portability.
       
   377 \<close>
   370 \<close>
   378 
   371 
   379 subsubsection \<open>Examples\<close>
   372 subsubsection \<open>Examples\<close>
   380 
   373 
   381 text \<open>
   374 text \<open>