Re: Thoughts on committers pushing simple changes from other committers?

[Leo Famulari]

On Tue, Feb 21, 2023 at 12:54:32PM +0000, Christopher Baines wrote:
> Thoughts?

I think it's fine to push other people's patches. Already, we push the
patches of non-committers. It's no big deal to push committers' patches.