> Strip the accidental changes from the repository? Never strip public changesets.
> 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" Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
