I understand the frustrations around closing somebody’s PR as stale, but I also think that there is value in informing the contributors I this is never getting solved/fixed/looked at, if this is still important please go over there instead.
On Mon, Nov 29, 2021 at 1:55 PM Robert Muir <[email protected]> wrote: > On Mon, Nov 29, 2021 at 2:49 PM Michael McCandless > <[email protected]> wrote: > > > > Could we maybe instead bulk-add a comment explaining the split and how > to take the PR forwards if someone (in the future) has itch/time? > > > > I know we humans love to clean things up, but I think leaving such > "unclean" things open serves an important purpose. They all had importance > to at least one person at one point in time, and likely many of them are > still relevant if they piqued someones curiosity to dig back into them. > Closing them makes them harder to find for the future developer. > > > > I'm sure some of them are already resolved/duplicates too. If only we > could divine which are which. > > > > > > +1, I'd rather not auto-close PRs. I'm always frustrated by this when > I see it in other trackers. Is there a rush to close these for some > reason? > > --------------------------------------------------------------------- > To unsubscribe, e-mail: [email protected] > For additional commands, e-mail: [email protected] > >
