--- a/src/Doc/System/Misc.thy Mon May 30 10:51:04 2022 +0200
+++ b/src/Doc/System/Misc.thy Mon May 30 10:52:00 2022 +0200
@@ -313,7 +313,7 @@
Options are:
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
- -P NAME protect NAME within TARGET from deletion
+ -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
-R ROOT explicit repository root directory
(default: implicit from current directory)
-T thorough check of file content (default: time and size)
@@ -342,8 +342,8 @@
for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
to force actual deletions on the target.
- \<^medskip> Option \<^verbatim>\<open>-P\<close> protects a given file or directory from deletion; multiple
- \<^verbatim>\<open>-P\<close> options may be given to accumulate protected entries.
+ \<^medskip> Option \<^verbatim>\<open>-F\<close> adds a filter rule to the underlying \<^verbatim>\<open>rsync\<close> command;
+ multiple \<^verbatim>\<open>-F\<close> options may be given to accumulate a list of rules.
\<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default
is to derive it from the current directory, searching upwards until a
@@ -356,9 +356,8 @@
subsubsection \<open>Examples\<close>
text \<open>
- Synchronize the Isabelle repository onto a remote host, while
- protecting a copy of AFP inside of it (without changing that):
- @{verbatim [display] \<open> isabelle hg_sync -R '$ISABELLE_HOME' -P AFP -C testmachine:test/isabelle\<close>}
+ Synchronize the Isabelle repository onto a remote host:
+ @{verbatim [display] \<open> isabelle hg_sync -R '$ISABELLE_HOME' -C testmachine:test/isabelle\<close>}
So far, this is only a dry run. In a realistic situation, it requires
consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
--- a/src/Pure/General/mercurial.scala Mon May 30 10:51:04 2022 +0200
+++ b/src/Pure/General/mercurial.scala Mon May 30 10:52:00 2022 +0200
@@ -486,7 +486,7 @@
Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
Scala_Project.here, { args =>
var clean = false
- var protect: List[String] = Nil
+ var filter: List[String] = Nil
var root: Option[Path] = None
var thorough = false
var dry_run = false
@@ -499,7 +499,7 @@
Options are:
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
- -P NAME protect NAME within TARGET from deletion
+ -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
-R ROOT explicit repository root directory
(default: implicit from current directory)
-T thorough check of file content (default: time and size)
@@ -512,7 +512,7 @@
which can be local or remote (using notation of rsync).
""",
"C" -> { _ => clean = true; dry_run = true },
- "P:" -> (arg => protect = protect ::: List(arg)),
+ "F:" -> (arg => filter = filter ::: List(arg)),
"R:" -> (arg => root = Some(Path.explode(arg))),
"T" -> (_ => thorough = true),
"f" -> (_ => dry_run = false),
@@ -534,8 +534,7 @@
case None => the_repository(Path.current)
}
hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
- dry_run = dry_run, clean = clean, rev = rev,
- filter = protect.map("protect /" + _))
+ dry_run = dry_run, clean = clean, filter = filter, rev = rev)
}
)
}