[isabelle-dev] "Divergent renames"

[Stefan Berghofer]

Quoting Makarius <makarius at sketis.net>:
> On Thu, 1 Dec 2011, Jasmin Christian Blanchette wrote:
>
>> I just pulled and updated ("hg pull -u") from the main repository  
>> and got these strange warnings:
>>
>> Fügte 118 Änderungssätze mit 572 Änderungen zu 411 Dateien hinzu
>> warning: detected divergent renames of src/Pure/General/markup.ML to:
>> [...]
>>
>> Anybody knows whether they're harmful?
>
> 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".

Hi,

I just got the very same warnings when updating my copy of the Isabelle
sources. I already got similar warning messages

   warning: detected divergent renames of  
src/HOL/Tools/Sledgehammer/sledgehammer.ML to:
   src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
   src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

a while ago (January 2011). When I asked Markus about this, he replied to
me that he had noticed them as well, but ignored it, and that he had not
discovered any negative effects so far. Maybe it is time to look at this
issue again rather than ignoring it?

Greetings,
Stefan