There's no reason for the dev list to get spammed everytime there's a github PR. We know most of the time we prefer JIRAs for real code PRs, but with docs being in tree and low barrier to entry, we may want to accept docs through PRs ( see https://issues.apache.org/jira/browse/CASSANDRA-13256 , and comment on it if you disagree).
To make that viable, we should make it not spam dev@ with every comment. Therefore I propose we move github PR comments/actions to pr@ so as not to clutter the dev@ list. Voting to remain open for 72 hours. - Jeff
