I would be inclined to forgo @-mentioning folks and let the core developers use their own ways of monitoring the activity on GitHub (subscribing to repo notifications; Octobox; personal GitHub API integrations, etc.).
I would be inclined to forgo @-mentioning folks and let the core developers use their own ways of monitoring the activity on GitHub (subscribing to repo notifications; Octobox; personal GitHub API integrations, etc.).