On Sun, Dec 17, 2023 at 11:37:23PM +0100, Pascal Quantin wrote:
> 17 déc. 2023 23:29:59 Guy Harris :
>
> > On Dec 17, 2023, at 10:08 AM, Jaap Keuter wrote:
> >
> >> 1. The GitHub mirror is picking up all our cherry-pick branches, which now
> >> run in the hundreds.
> >
> > 1.5. Are cherry-pick
17 déc. 2023 23:29:59 Guy Harris :
> On Dec 17, 2023, at 10:08 AM, Jaap Keuter 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 vers
On Dec 17, 2023, at 10:08 AM, Jaap Keuter 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
