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: [email protected] <[email protected]> On Behalf Of Ard > Biesheuvel > Sent: Monday, May 6, 2024 3:01 AM > To: [email protected]; Kinney, Michael D <[email protected]> > Cc: Pedro Falcato <[email protected]>; [email protected]; Leif > Lindholm <[email protected]>; Andrew Fish ([email protected]) > <[email protected]> > 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 <[email protected]> > 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: [email protected] Unsubscribe: https://edk2.groups.io/g/devel/unsub [[email protected]] -=-=-=-=-=-=-=-=-=-=-=-
