17 déc. 2023 23:29:59 Guy Harris <gharris@xxxxxxxxx>:
> 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.
They are deleted most of the time (when the option is checked in GitLab UI, which is the default value). Once in a while I delete a few stale merge branches that stay open because the corresponding merge requests were closed or because the delete option was not selected, to keep our branches number under control.