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? 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.