The following situation has happened to me several times: Someone writes a comment tagging me with the @, I read the comment, and shortly after the comment is edited in such a way that the nature of the comment is completely changed, after which I see it maybe an hour later if at all. I would bet that there are at least a few that I have missed completely. I've observed that the situation has also happened at least once in reverse (I edited a comment and the person didn't see the edit until I pointed it out).
Is it feasible to have a user that is tagged in a comment be notified whenever a comment they are tagged in is edited?
EDIT: Other methods of notification, even if it does not involve the pinging, would also be good, such as what happens when posts are edited or comments are added when you're on the page. This won't be visible on the android app, I assume, which is where I spend most of my site time, but it would fix the problem in the browser at least.
EDIT EDIT: has this been implemented? I think I just got notified in the android app when someone edited a comment. I got a ping but no new comment in the view, and I checked and the comment was edited.
@
pings. $\endgroup$