[isabelle-dev] More Mercurial hints

[Makarius]

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 
   merges.

   hg fetch is configured by putting something like this into your local 
   ~/.hgrc

     [extensions]
     hgext.fetch =

     [defaults]
     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:

     [trusted]
     users = wenzelm

   This needs to be added to ~/.hgrc on the server side within the broy 
   network at TUM.


	Makarius