Hi
[Resending with better compressed attachment, because 30k limit]
first off: I don't care particularly strongly about this matter. I would
be in favor of cleaning out the old branches, but I'm also not in a
position to tell others how to do their job.
On 12/14/22 21:04, Sara Golemon wrote:
On Tue, Dec 13, 2022 at 12:03 PM Tim Düsterhus wrote:
> One benefit of removing those branches would be, that usability of
> GitHub's branch selector improves, specifically the branch selector when
> creating a new PR.
>
Maybe this is my CLI privilege talking, but who's using pulldowns to select
Hi
On 12/13/22 18:55, Sara Golemon wrote:
Why do you want to remove these branches?
I agree that they have minimal value especially since the tags are the
actual release commit (and for release process versions often represent a
spur off the release branch), but the cost in the repo is negligib
On Tue, Dec 13, 2022 at 11:31 AM Michael Voříšek - ČVUT FJFI <
voris...@fjfi.cvut.cz> wrote:
> Hello everyone,
>
> I am the author of https://github.com/php/php-src/issues/10007 proposal
> and I would ask you for the green light to do so.
>
>
Why do you want to remove these branches?
I agree that
