+1
> On Sep 23, 2021, at 2:23 AM, Stamatis Zampetakis <zabe...@gmail.com> wrote: > > 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
