On Thursday, August 22, 2024 at 3:32:16 PM UTC-7 Matthias Koeppe wrote: On Thursday, August 22, 2024 at 2:19:36 PM UTC-7 David Roe wrote:
We are starting this thread for two reasons. 1. Kwankyu asked for clarity on who can mark comments as off topic. 2. You marked this comment <https://github.com/sagemath/sage/pull/38219#issuecomment-2283629487> as off-topic, which asked for clarification on the action you had just taken removing the disputed label, and then several additional comments on that PR. Since our project is fairly new to github, we have not yet developed norms for using its moderation features. We are starting this thread to discuss such norms with the community. We made one proposal, but are open to others, which is why we asked for discussion rather than a vote. Forgive me for using the Socratic method, but do you understand what the function of this standard GitHub functionality ("mark comment as off-topic") is? I'll help: Per https://docs.github.com/en/communities/moderating-comments-and-conversations/managing-disruptive-comments "Organization moderators, and anyone with write access to a repository, can hide comments on issues, pull requests, and commits. If a comment is off-topic, outdated, or resolved, you may want to hide a comment to keep a discussion focused or make a pull request easier to navigate and review. Hidden comments are minimized but people with read access to the repository can expand them." You will note that the reasons for hiding comments as off-topic, outdated, or resolved are entirely practical. It has nothing to do with "conduct". It's therefore in the realm of Maintainer actions and outside of the narrow charge of the CoC committee. -- 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/728af24f-414e-410e-b5ff-2da2db3f95edn%40googlegroups.com.
