Stream: Coq devs & plugin devs

Topic: Resolving PR Feedback


view this post on Zulip Janno (May 28 2020 at 12:48):

What's the policy on resolving feedback in PRs for the PR author? GitHub has the "Resolve Conversation" button that I can click (hopefully because I am the author, not because I've got too many permissions in the repo). My feeling was that whoever wrote the comment would resolve it once the requested changes happen or once the feedback has been addressed in some other way. How do others handle this?

view this post on Zulip Théo Zimmermann (May 28 2020 at 12:51):

If there are many comments and that you are sure your resolved a review comment, it is best that you click the button yourself, because this will help both you and the reviewers skim more quickly through comments that are not marked as resolved yet.

view this post on Zulip Théo Zimmermann (May 28 2020 at 12:51):

However, if you answered a review comment, do not resolve it, otherwise the reviewer is likely to miss your answer.

view this post on Zulip Janno (May 28 2020 at 12:52):

Okay, I see.. should I be pinging people who've not reacted to my answers then? (If so, what's the polite time to wait before pinging? :D)

view this post on Zulip Théo Zimmermann (May 28 2020 at 12:54):

Well, it depends on their usual reactiveness, but you should probably wait a few days before pinging.

view this post on Zulip Janno (May 28 2020 at 12:55):

Makes sense! Thank you!

view this post on Zulip Enrico Tassi (May 28 2020 at 12:56):

Janno said:

Okay, I see.. should I be pinging people who've not reacted to my answers then? (If so, what's the polite time to wait before pinging? :D)

Yes do, we (reviewers) are often flooded by github notifications, and sometimes it hard to understand weather it means "all done, please check again" or "some work done, please come back later". Or at least, this holds for me.


Last updated: Oct 13 2024 at 01:02 UTC