clarified documentation: $ISABELLE_HOME is not a repository for regular releases;
authorwenzelm
Mon, 30 May 2022 10:56:51 +0200
changeset 75490 5e37ea93759d
parent 75489 f08fd5048df3
child 75491 47d790984e82
clarified documentation: $ISABELLE_HOME is not a repository for regular releases;
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.