On Dec 17, 2023, at 10:08 AM, Jaap Keuter <jaap.keuter@xxxxxxxxx> wrote:
> 1. The GitHub mirror is picking up all our cherry-pick branches, which now run in the hundreds.
1.5. Are cherry-pick branches deleted once the changes on those branches are merged into the version branch and, if not, why not? Do they serve some purpose such as recording history that is, in some fashion, of interest? The changes themselves are in the version branch and, by default, the commit message includes the signature of the commit from which it was cherry-picked.