Should we use branches?

[Lawrence Paulson]

One thing I've noticed at Amazon is that they insist on a single threaded revision trail. They do this by requiring everybody to make their changes within a personal branch, which they then re-base to the main branch before pushing. Sometimes they also merge adjacent commits. In return for mastering a couple of extra commands, everybody benefits from a much cleaner revision history. Do we want to try this?

Larry
[cid:6ce32522-80e2-4611-8cd1-3eecd6e69d1d at GBRP265.PROD.OUTLOOK.COM]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250516/e108a2cc/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hg.jpeg
Type: image/jpeg
Size: 99363 bytes
Desc: hg.jpeg
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250516/e108a2cc/attachment-0001.jpeg>