--- a/src/Doc/System/Misc.thy Sun May 29 17:37:43 2022 +0200
+++ b/src/Doc/System/Misc.thy Sun May 29 20:57:10 2022 +0200
@@ -303,9 +303,9 @@
section \<open>Mercurial repository synchronization\<close>
text \<open>
- The @{tool_def hg_sync} tool synchronizes the working directory of a local
- Mercurial repository with a target directory, using
- \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for destinations.
+ The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
+ a target directory, using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close>
+ notation for destinations.
@{verbatim [display]
\<open>Usage: isabelle hg_sync [OPTIONS] TARGET
@@ -318,15 +318,19 @@
(default: implicit from current directory)
-f force changes: no dry-run
-n no changes: dry-run
+ -r REV explicit revision (default: state of working directory)
-v verbose
- Synchronize Mercurial repository working directory with other TARGET,
+ Synchronize Mercurial repository with TARGET directory,
which can be local or remote (using notation of rsync).\<close>}
The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
using \<^verbatim>\<open>rsync\<close> notation (see examples below). The content is written
directly into the target, \<^emph>\<open>without\<close> creating a separate sub-directory.
+ \<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
+ is the current state of the working directory (which might be uncommitted).
+
\<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode:
operations are only simulated and printed as in verbose mode. Option \<^verbatim>\<open>-f\<close>
disables ``dry-run'' mode and thus forces changes to be applied.
@@ -341,8 +345,8 @@
\<^verbatim>\<open>-P\<close> options may be given to accumulate protected entries.
\<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default
- is to derive it from the current working directory, searching upwards until
- a suitable \<^verbatim>\<open>.hg\<close> directory is found.
+ is to derive it from the current directory, searching upwards until a
+ suitable \<^verbatim>\<open>.hg\<close> directory is found.
\<close>
subsubsection \<open>Examples\<close>