On Tue, 7 Feb 2023, 11:33 'Martin R' via sage-devel, < sage-devel@googlegroups.com> wrote:
> Has there been already a decision how we incorporate the real name > "Author" and "Reviewer" fields? > > I think that this is rather important, because not making a decision will > probably also be a decision - there are already several new pull requests. > > Personally, I am very much for continuing the tradition of real names, but > it is not clear to me whether there is a mapping between user name and real > name on github anyway, which would make this information redundant. Is the > "Name" in a github account optional? > yes, names are optional on GitHub, so we will need some kind of mapping to keep. We can also get names of authors and reviewers in the PR description enforced by a bot. We can also require this info to be put in a special textfile to be collected at merging time and put into a changelog file. (amending changelog directly is prone to conflicts). > Martin > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/c2c8654a-0511-43a7-a7e5-66c6e687178an%40googlegroups.com > <https://groups.google.com/d/msgid/sage-devel/c2c8654a-0511-43a7-a7e5-66c6e687178an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/CAAWYfq3n4F63mmqdvOoVcMEvX0ngi9zDb9u85x%2BDy2VjuqkryA%40mail.gmail.com.
