Hi Ard, Thais is an attribute of Mergify. I do not see a way to change that behavior.
I do not know if using the GitHub merge capability or other merge services provides different behavior here or not. This specific request is not related to the change to GitHub PRs for code review. There is no intention to change the requirement for a maintainer to set the 'push' label and no intention to change away from Mergify at this time. Perhaps we can open your request as an independent request that we can find an owner to evaluate options and provide recommendations. Thanks, Mike > -----Original Message----- > From: Ard Biesheuvel <a...@kernel.org> > Sent: Monday, May 6, 2024 8:31 AM > To: Kinney, Michael D <michael.d.kin...@intel.com> > Cc: r...@edk2.groups.io; devel@edk2.groups.io; Pedro Falcato > <pedro.falc...@gmail.com>; Leif Lindholm <l...@nuviainc.com>; Andrew > Fish (af...@apple.com) <af...@apple.com> > Subject: Re: [edk2-rfc] [edk2-devel] Proposal to switch TianoCore Code > Review from email to GitHub Pull Requests on 5-24-2024 > > On Mon, 6 May 2024 at 17:11, Kinney, Michael D > <michael.d.kin...@intel.com> wrote: > > > > That information is in GitHub in the PR conversation. > > > > If you follow the link from the commit to the PR, the PR conversation > shows > > who set the 'push' label. > > > > But that is GitHub proprietary metadata, no? Is it not possible to set > the committer field in Git itself to something meaningful? -=-=-=-=-=-=-=-=-=-=-=- Groups.io Links: You receive all messages sent to this group. View/Reply Online (#118602): https://edk2.groups.io/g/devel/message/118602 Mute This Topic: https://groups.io/mt/105873467/21656 Group Owner: devel+ow...@edk2.groups.io Unsubscribe: https://edk2.groups.io/g/devel/unsub [arch...@mail-archive.com] -=-=-=-=-=-=-=-=-=-=-=-
