Suppose I created an issue on GitHub, or a pull request that improves something. Is there a standard procedure to attract some attention to it, so that it could be reviewed/fixed/merged?
I assume that I need to
@mention some core developers that can help. How do I know which ones to ping, if it’s not about a package (and thus there is no clearly defined maintainer)?
If someone already commented on the issue or PR, asked questions, received responses, and then seemingly forgot about it, how long should I wait before I try to send a reminder?