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.
Mike > -----Original Message----- > From: r...@edk2.groups.io <r...@edk2.groups.io> On Behalf Of Ard > Biesheuvel > Sent: Monday, May 6, 2024 3:01 AM > To: devel@edk2.groups.io; Kinney, Michael D <michael.d.kin...@intel.com> > Cc: Pedro Falcato <pedro.falc...@gmail.com>; r...@edk2.groups.io; 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 > > This reminds me: would it be possible to keep track of who merged a > PR? (i.e., the person that set the 'push' label) > > Currently, commits just appear on the branch with the original author > and the committer field set to something non-descript, e.g., > > commit 275d0a39c42ad73a6e4929822f56f5d8c16ede96 (HEAD -> master, > origin/master, origin/HEAD) > Author: Gerd Hoffmann <kra...@redhat.com> > AuthorDate: Fri Mar 1 08:44:00 2024 +0100 > Commit: mergify[bot] > <37929162+mergify[bot]@users.noreply.github.com> > CommitDate: Fri Mar 1 18:47:27 2024 +0000 > > which means we cannot tell from the git history which maintainer merged > this. > > > > -=-=-=-=-=-=-=-=-=-=-=- Groups.io Links: You receive all messages sent to this group. View/Reply Online (#118600): https://edk2.groups.io/g/devel/message/118600 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] -=-=-=-=-=-=-=-=-=-=-=-
