[isabelle-dev] More Mercurial hints

[Makarius]

On Mon, 2 Feb 2009, Makarius wrote:

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

Just as a reminder ...

It is important to develop a habit of doing fetch before any local edits, 
otherwise the history will become a chaos. (While I did produce a merge 
edge of 3 weeks length myself, I have an excuse: *no* network access 
during all that time.)


	Makarius