Should we use branches?

[Fabian Huch]

On 5/16/25 13:22, Gerwin Klein via isabelle-dev wrote:
> It’s possible to do in hg, but not as nicely

Actually I find it much easier to do such operations in hg: Because it 
allows you to simply talk about changesets, all the operations and 
commands get a lot easier (especially for beginners!).

E.g. to rebase one commit onto another you just do

hg rebase --source xxx --dest yyy

And the histedit extension allows you to do a lot more operations with 
ease as well.

> and needs people who know how to deal with it. 

That's certainly a problem.


Fabian