Hi all, Currently we are supposed to append the contributors name to the commit summary when they are not committers of the project. The main reason for doing this if I am not mistaken is to give some credit to those people.
I did like this practice in the beginning but I think it adds some small overhead to all parties involved (committers and contributors). The contributor quite often forgets to include the name in the end so the burden to find and append the name goes to the committer. In various cases, I've seen PRs ready to merge which were actually missing the name at the end. What usually happens afterwards is one of the following: * the committer merges the PR without amending the name; * the committer rebases the PR, amends the commit, and merges it; * the committer asks the contributor to change the commit message; I would prefer it if we could avoid this overhead by changing the commit guidelines to not append the contributors name at the end. GitHub does a great job giving credit to contributors. Moreover in most cases the name appears in the log under the author tag so it is very easy to exploit if we want to extract information and statistics. What do you think? Best, Stamatis
