Hi all,
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:
src/Pure/PIDE/isabelle_markup.ML
* Renamed inner syntax categories num to num_token and xnum to
xnum_token, in accordance to existing float_token. Minor
INCOMPATIBILITY. Note that in practice num_const etc. are mainly
used instead.
This refers to Isabelle/c7a13ce60161.
Makarius
On Thu, 1 Dec 2011, Jasmin Christian Blanchette wrote:
Hi all,
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
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
Quoting Makarius makar...@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
Am 01.12.2011 um 13:06 schrieb Stefan Berghofer:
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:
On Thu, 1 Dec 2011, Jasmin Blanchette wrote:
Am 01.12.2011 um 13:06 schrieb Stefan Berghofer:
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
