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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
