For the records, when pushing manually a commit from a PR as it is, the initial author of the commit can be preserved via git commit --author="..." .... The author can be taken from the patch of the PR.


You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.