46 name is specified. The full repository meta-data and history of |
46 name is specified. The full repository meta-data and history of |
47 changes is in isabelle/.hg; local configuration for this clone can be |
47 changes is in isabelle/.hg; local configuration for this clone can be |
48 added to isabelle/.hg/hgrc, but note that hgrc files are never copied |
48 added to isabelle/.hg/hgrc, but note that hgrc files are never copied |
49 by another clone operation! |
49 by another clone operation! |
50 |
50 |
|
51 |
51 There is also $HOME/.hgrc for per-user Mercurial configuration. The |
52 There is also $HOME/.hgrc for per-user Mercurial configuration. The |
52 initial configuration should include at least an entry to identify |
53 initial configuration should include at least an entry to identify |
53 yourself. For example, something like this in /home/wenzelm/.hgrc: |
54 yourself. For example, something like this in /home/wenzelm/.hgrc: |
54 |
55 |
55 [ui] |
56 [ui] |
56 username = wenzelm |
57 username = wenzelm |
57 |
58 |
58 Failing to configure the username correctly makes the system invent |
59 Of course, the user identity can be also configured in |
59 funny machine names that may persist indefinitely in the public flow |
60 isabelle/.hg/hgrc on per-repitory basis. Failing to specify the |
60 of changesets. |
61 username correctly makes the system invent funny machine names that |
|
62 may persist indefinitely in the public flow of changesets. |
61 |
63 |
62 In principle, user names can be chosen freely, but for longterm |
64 In principle, user names can be chosen freely, but for longterm |
63 committers of the Isabelle repository the obvious choice is to keep |
65 committers of the Isabelle repository the obvious choice is to keep |
64 with the old CVS naming scheme. |
66 with the old CVS naming scheme. |
65 |
67 |