[isabelle-dev] mercurial accident

[Tobias Nipkow]

Hey, I wanted to join the party! But all bugs have been fixed now and Makarius 
will notify you of the correct changeset.

Tobias

On 18/01/2019 21:42, Makarius wrote:
> On 17/01/2019 22:54, Fabian Immler wrote:
>>
>> Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong
>> during the merges, so I could easily redo Angeliki's tagging (689997a8).
>>
>> We should be back to normal (regarding isabelle build -a).
> 
> That was Isabelle/94284d4dab98, but Tobias has just pushed a bad merge
> again: Isabelle/aeceb14f387a.
> 
> I can only quote README_REPOSITORY once more:
> 
> 
> Testing of changes (before push)
> --------------------------------
> 
> The integrity of the standard pull/push area of Isabelle needs the be
> preserved at all time.  This means that a complete test with default
> configuration needs to be finished successfully before push.  If the
> preparation of the push involves a pull/merge phase, its result needs
> to covered by the test as well.
> 
> 
> Such testing of local changes plus the resulting merge is not optional,
> but mandatory.
> 
> There is a natural routine of "hg commit" vs. "isabelle build -a" to
> make it all work well without any effort.
> 
> 
> 	Makarius
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190118/ca375d7f/attachment.bin>