# HG changeset patch
# User wenzelm
# Date 1653901011 -7200
# Node ID 5e37ea93759d2ef58190b4b17f81261a41666ddf
# Parent  f08fd5048df31bb6c9e32c3586f44744c410dc64
clarified documentation: $ISABELLE_HOME is not a repository for regular releases;

diff -r f08fd5048df3 -r 5e37ea93759d src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Mon May 30 10:52:00 2022 +0200
+++ b/src/Doc/System/Misc.thy	Mon May 30 10:56:51 2022 +0200
@@ -356,8 +356,9 @@
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Synchronize the Isabelle repository onto a remote host:
-  @{verbatim [display] \<open>  isabelle hg_sync -R '$ISABELLE_HOME' -C testmachine:test/isabelle\<close>}
+  Synchronize the current repository onto a remote host, with accurate
+  treatment of all files (concerning comparison and deletion on target):
+  @{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
   consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.