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


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.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to