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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
