equal
deleted
inserted
replaced
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> |