[isabelle-dev] mercurial accident

[Makarius]

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