A separate but related question: should we give people credit for their contributions in the release notes? We could append a contributor’s name to each contribution (achieving a similar effect to today). Or we could generate a “The following people contributed to this release: …” paragraph per release. Or let people’s contributions speak for themselves (if you want to know who did a change, browse GitHub).
I lean towards the last of these, but I want to hear what others think. The goal, as ever, is to build a strong community. Julian > On Sep 23, 2021, at 7:37 AM, Julian Hyde <[email protected]> wrote: > > +1 > >> On Sep 23, 2021, at 2:23 AM, Stamatis Zampetakis <[email protected]> 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
