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