[isabelle-dev] More Mercurial hints
makarius at sketis.net
Mon Feb 2 17:48:52 CET 2009
A few more hints on using the Isabelle Mercurial repository smoothly,
although most people should now this already.
* The fetch extension takes care of most of the details of
pull/update/merge, asking for user intervention only for non-trivial
hg fetch is configured by putting something like this into your local
fetch = -m "merged"
The default merge message is used for all trivial (automatic) merges.
Of course, if a merge is non-trivial, the message should indicate this.
In the latter case the message is entered manually via the usual
interactive editor popup.
* Merges can be simplified by doing "hg fetch" frequently, especially
just before starting to perform local edits. Also do not forget to
push eventually, to give others a chance to pick up the changes.
Note that excessively long merge edges will make the cumulative history
hard to follow later on. The history is very important to understand
how the sources emerge; inspecting the history is routinely required
whenever a problem or unclarity arises.
* Funny warnings about Mercurial not trusting the default hgrc of the
central pull/push area can be disabled like this:
users = wenzelm
This needs to be added to ~/.hgrc on the server side within the broy
network at TUM.
More information about the isabelle-dev