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