awaiting-author label was not removed

Stream: mathlib4

[Etienne Marion]

In #34542 the awaiting-author label was not removed after the author commented -awaiting-author. I am guessing this is not normal, can somebody have a look please?

[Bryan Gin-ge Chen]

Next to the author's comment, there's a "View reviewed changes" link, so I think that it's actually a "pull request review" not an ordinary comment on the PR. I'll look into making the bot respond to reviews and review comments as well.

[Etienne Marion]

Thanks I did not notice that! It is unexpected that one would deal with labels through review comments.

[Bryan Gin-ge Chen]

Indeed, the fact that there are 3 types of these comment-adjacent things has been the source of many headaches in our workflows...

[Bryan Gin-ge Chen]

#34549 should make the bot trigger on reviews + review comments as well.