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
squared.
>
>> 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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
