[isabelle-dev] "Divergent renames"

[Alexander Krauss]

On 12/01/2011 01:33 PM, Jasmin Blanchette wrote:
> According to Brian, who should be coming back from the coffee break
> in 15 minutes or so, these things happen when you effectively split a
> file into two -- like I did in January with "sledgehammer.ML".
> There's apparently some heuristic in Mercurial that tries to detects
> clones and relabel them as renames, and that heuristic kind of goes
> crazy when you split a file into two.

As far as I understand there is no heuristic involved here. Rather I 
think it is the issue described here:

http://mercurial.selenic.com/bts/issue2113

So it seems the warning, which is intended for a different situation, is 
harmless when you are not really merging and should not be there in the 
first place. It can be ignored, unless you have some special business 
with the mentioned files.

Alex