[isabelle-dev] mercurial accident

Makarius makarius at sketis.net
Thu Jan 17 21:54:34 CET 2019

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.


More information about the isabelle-dev mailing list