[isabelle-dev] Isabelle on Mercurial

[Makarius]

There is a useful convenience for synchronizing a local repository with 
changes that have accumulated on the pull/push area: see "hg fetch" in the 
Mercurial book http://hgbook.red-bean.com or the wiki.

The relevant section from the book is attached below.

The "fetch" command automatically handles routine merges, and clearly 
indicates so in the log entry.  A non-trivial situation needs to be 
handled separately, with hand-written log entry as appropriate to the 
situation.  In most cases the message should be just "merged", unless a 
real semantic conflict was resolved.


	Makarius

===========================================================================
3.3  Simplifying the pull-merge-commit sequence

The process of merging changes as outlined above is straightforward, but 
requires running three commands in sequence.
  hg pull
  hg merge
  hg commit -m 'Merged remote changes'

In the case of the final commit, you also need to enter a commit message, 
which is almost always going to be a piece of uninteresting "boilerplate" 
text.

It would be nice to reduce the number of steps needed, if this were 
possible. Indeed, Mercurial is distributed with an extension called fetch 
that does just this.

Mercurial provides a flexible extension mechanism that lets people extend 
its functionality, while keeping the core of Mercurial small and easy to 
deal with. Some extensions add new commands that you can use from the 
command line, while others work "behind the scenes," for example adding 
capabilities to the server.

The fetch extension adds a new command called, not surprisingly, "hg 
fetch". This extension acts as a combination of "hg pull", "hg update" and 
"hg merge". It begins by pulling changes from another repository into the 
current repository. If it finds that the changes added a new head to the 
repository, it begins a merge, then commits the result of the merge with 
an automatically-generated commit message. If no new heads were added, it 
updates the working directory to the new tip changeset.

Enabling the fetch extension is easy. Edit your .hgrc, and either go to 
the [extensions] section or create an [extensions] section. Then add a 
line that simply reads "fetch ".
  [extensions]
  fetch =

(Normally, on the right-hand side of the "=" would appear the location of 
the extension, but since the fetch extension is in the standard 
distribution, Mercurial knows where to search for it.)
===========================================================================