Here a development infrastructure feature was designed and implemented by a new contributor. This rare engagement with the development infrastructure of the project is something that our community should welcome and encourage
The feature was introduced through the normal process. At lease three people welcomed the new contributor. Claiming that there should have been a discussion in sage-devel before merging the PR is asking too much. There is no clearcut of what to discuss here or what not. But now we are discussing about the feature, not about the PR of the new contributor. As we have some experiences with the feature, we can now discuss whether to keep it or not. -- 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/432fd987-b828-4691-8c97-2284cf037b1an%40googlegroups.com.