README_REPOSITORY
changeset 28917 20f43e0e0958
parent 28913 86ed1c86e0ef
child 28918 eda3d9976ec7
     1.1 --- a/README_REPOSITORY	Sun Nov 30 14:03:46 2008 +0100
     1.2 +++ b/README_REPOSITORY	Sun Nov 30 14:43:29 2008 +0100
     1.3 @@ -48,6 +48,7 @@
     1.4  added to isabelle/.hg/hgrc, but note that hgrc files are never copied
     1.5  by another clone operation!
     1.6  
     1.7 +
     1.8  There is also $HOME/.hgrc for per-user Mercurial configuration.  The
     1.9  initial configuration should include at least an entry to identify
    1.10  yourself.  For example, something like this in /home/wenzelm/.hgrc:
    1.11 @@ -55,9 +56,10 @@
    1.12    [ui]
    1.13    username = wenzelm
    1.14  
    1.15 -Failing to configure the username correctly makes the system invent
    1.16 -funny machine names that may persist indefinitely in the public flow
    1.17 -of changesets.
    1.18 +Of course, the user identity can be also configured in
    1.19 +isabelle/.hg/hgrc on per-repitory basis.  Failing to specify the
    1.20 +username correctly makes the system invent funny machine names that
    1.21 +may persist indefinitely in the public flow of changesets.
    1.22  
    1.23  In principle, user names can be chosen freely, but for longterm
    1.24  committers of the Isabelle repository the obvious choice is to keep