# HG changeset patch
# User wenzelm
# Date 1653904294 -7200
# Node ID f775dfb556552be002c3e5e9b15f7fe4c91199e1
# Parent  c03c2bf4ef8ab4d6a58c724976d5189e646f5f08
clarified option -T;

diff -r c03c2bf4ef8a -r f775dfb55655 src/Doc/System/Misc.thy
--- 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
diff -r c03c2bf4ef8a -r f775dfb55655 src/Pure/Admin/sync_repos.scala
--- 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
diff -r c03c2bf4ef8a -r f775dfb55655 src/Pure/General/mercurial.scala
--- 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)
diff -r c03c2bf4ef8a -r f775dfb55655 src/Pure/System/isabelle_system.scala
--- 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 +