# HG changeset patch # User wenzelm # Date 1228052609 -3600 # Node ID 20f43e0e09583e3c912406d7f704ef026c7d1ed4 # Parent 0a802cdda3407b85a4d66759ed09fddba953c05a tuned; diff -r 0a802cdda340 -r 20f43e0e0958 README_REPOSITORY --- 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 @@ [ui] 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