Send a message on GitHub when a duplicate preflight poll terminates.

[zli-simspace]

Gonna preface this by saying I'm not super sure about this one.

Background

I'm trying to track down why the prefilight poll sometimes terminates when there are no duplicates. Excerpt from the logs.

[info] Continue Poll Patch 10349 prerun
[info] Code review status: Label Check true Passed Status: false Passed Review: sufficient CODEOWNERS: true Passed Up-To-Date Review: sufficient
<Some GitHub webhooks happen>
[info] Continue Poll Patch 10349 prerun
[info] Patch 10349 already left prerun, exiting prerun poll loop

I see the extra already left prerun check was added in #841 and its only supposed to remove duplicate bors r+/merge requests. But I don't see any duplicate requests here: the timestamps of Continue Poll are about a minute apart and there are no new Start Poll Patch).

I see other cases where Bors comments with "Waiting for PR Status" and then doesn't comment again (or merge) and suspect is a similar issue, but the logs are too far back and we don't have then anymore.

Since the polling silently stops, its quite frustrating for devs who have to bors r+ again.

Solution

In this PR, Bors adds a GitHub comment when it stops polling due to duplicates. This should both inform devs and help track down this issue.

Drawbacks

This add an extra comment from Bors, which may sometimes be confusing. But if people made multiple requests, they should understand the messages referring to duplicates. It is only in the case where the preflight polling stopped due to something else where the message would be confusing. But I'm thinking even in that case, its better they are informed.

[notriddle]

This is working around a bug, so I don't like it very much, but TBF it is also probably worse having a message silently get thrown away.

Let's do it then. (/me holds nose)

bors r+

[bors]

Build succeeded:

• continuous-integration/travis-ci/push
• Community-TC (push)

[collares]

I see other cases where Bors comments with "Waiting for PR Status" and then doesn't comment again (or merge) and suspect is a similar issue, but the logs are too far back and we don't have then anymore.

Since the polling silently stops, its quite frustrating for devs who have to bors r+ again.

@zli-simspace Not sure if this still bothers you, but I think I found a likely cause for this bug. It's described at #1434 (comment)