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 (#118593): https://edk2.groups.io/g/devel/message/118593 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] -=-=-=-=-=-=-=-=-=-=-=-
