--- a/src/Doc/System/Misc.thy Mon May 30 11:34:25 2022 +0200
+++ b/src/Doc/System/Misc.thy Mon May 30 11:51:34 2022 +0200
@@ -316,7 +316,7 @@
-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)
+ -T thorough treatment of file content and directory times
-f force changes: no dry-run
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
@@ -349,15 +349,16 @@
is to derive it from the current directory, searching upwards until a
suitable \<^verbatim>\<open>.hg\<close> directory is found.
- \<^medskip> Option \<^verbatim>\<open>-T\<close> indicates a thorough check of file content; the default is to
- consider files with equal time and size already as equal.
+ \<^medskip> Option \<^verbatim>\<open>-T\<close> indicates thorough treatment of file content and directory
+ times. The default is to consider files with equal time and size already as
+ equal, and to ignore time stamps on directories.
\<close>
subsubsection \<open>Examples\<close>
text \<open>
Synchronize the current repository onto a remote host, with accurate
- treatment of all files (concerning comparison and deletion on target):
+ treatment of all content:
@{verbatim [display] \<open> isabelle hg_sync -T -C remotename:test/repos\<close>}
So far, this is only a dry run. In a realistic situation, it requires
--- a/src/Pure/Admin/sync_repos.scala Mon May 30 11:34:25 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala Mon May 30 11:51:34 2022 +0200
@@ -68,7 +68,7 @@
-J preserve *.jar files
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
- -T thorough check of file content (default: time and size)
+ -T thorough treatment of file content and directory times
-a REV explicit AFP revision (default: state of working directory)
-f force changes: no dry-run
-n no changes: dry-run
--- a/src/Pure/General/mercurial.scala Mon May 30 11:34:25 2022 +0200
+++ b/src/Pure/General/mercurial.scala Mon May 30 11:51:34 2022 +0200
@@ -502,7 +502,7 @@
-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)
+ -T thorough treatment of file content and directory times
-f force changes: no dry-run
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
--- a/src/Pure/System/isabelle_system.scala Mon May 30 11:34:25 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon May 30 11:51:34 2022 +0200
@@ -433,7 +433,7 @@
val script =
"rsync --protect-args --archive" +
(if (verbose || dry_run) " --verbose" else "") +
- (if (thorough) " --ignore-times" else "") +
+ (if (thorough) " --ignore-times" else " --omit-dir-times") +
(if (dry_run) " --dry-run" else "") +
(if (clean) " --delete-excluded" else "") +
filter.map(s => " --filter=" + Bash.string(s)).mkString +