[isabelle-dev] "Divergent renames"

[Jasmin Blanchette]

Hi Makarius,

> Good question.  There is a brief explanation at
> http://hgbook.red-bean.com/read/mercurial-in-daily-use.html
> in the section "Divergent renames and merging".
> 
> Did it produce any merge node locally?  What does "hg out" say?

lapbroy152:HOL blanchet$ hg out
Vergleiche mit ssh://atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
Suche nach Änderungen
Keine Änderungen gefunden

I'm using patches, so I never (well, hardly ever) do any merges locally.

> BTW, what I've done here (d83797ef0d2d) with the files is to use "hg cp ..." and then edit both copies.

Jasmin