[isabelle-dev] For casual mercurial users

[Makarius]

On Wed, 11 Mar 2009, Florian Haftmann wrote:

> 	hg update -v
> 
> resp.
> 
> 	hg pull -u -v
> 
> This then imitates the CVS style output which tells explicitly which
> files receive changes, which is helpful to find out whether somebody
> else is working on the files I am currently editing.

Nice.  I did not know this yet.

Since -v is one of the generic options that apply to any command, one can 
also do this of course:

  hg fetch -v

As usual, user preferences can be added to the [defaults] section of 
~/.hgrc, for example:

  [defaults]
  fetch = -m "merged" -v


	Makarius