[isabelle-dev] mercurial accident
immler at in.tum.de
Thu Jan 17 22:54:51 CET 2019
Thanks for your feedback!
I did what Lars suggested (96a43caa).
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).
On 1/17/2019 3:54 PM, Makarius wrote:
> On 17/01/2019 21:42, Lars Hupel wrote:
>>> Strip the accidental changes from the repository?
>> Never strip public changesets.
> Indeed. "Fixing" a desaster by non-monotonic operations is a desaster
>>> Back out the changes?
>> You can't really back out merges, as far as I know.
>>> Or do a no-op merge from a successor of the last working version?
>> This is also not possible, I think.
>> Do this instead:
>> $ hg revert -a -r 56acd449da41
>> $ hg commit -m "revert to 56acd449da41"
> This looks fine and obvious.
> The problem behind this: Angeliki got administrative push-access to the
> Isabelle repository, without anybody at Cambridge showing her how to use it.
> There is of course README_REPOSITORY, but the text is long. Here is the
> ultra-short version:
> After every local commit, use "hg view" (or equivalent) to ensure that
> the change is really what you want to make eternal when pushed to public.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev