Sun, 30 Nov 2008 14:43:29 +0100
changeset 28917 20f43e0e0958
parent 28916 0a802cdda340
child 28918 eda3d9976ec7
--- a/README_REPOSITORY	Sun Nov 30 14:03:46 2008 +0100
+++ b/README_REPOSITORY	Sun Nov 30 14:43:29 2008 +0100
@@ -48,6 +48,7 @@
 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
 by another clone operation!
 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
 initial configuration should include at least an entry to identify
 yourself.  For example, something like this in /home/wenzelm/.hgrc:
@@ -55,9 +56,10 @@
   username = wenzelm
-Failing to configure the username correctly makes the system invent
-funny machine names that may persist indefinitely in the public flow
-of changesets.
+Of course, the user identity can be also configured in
+isabelle/.hg/hgrc on per-repitory basis.  Failing to specify the
+username correctly makes the system invent funny machine names that
+may persist indefinitely in the public flow of changesets.
 In principle, user names can be chosen freely, but for longterm
 committers of the Isabelle repository the obvious choice is to keep