AFAIK I don't think it's a bug in github-bot, but a Github UI bug? The labels were all added at the same time it looks like, so maybe a race condition issue on Github's end?

As the bot fetches the existing labels on a PR via the github API, before adding new ones which haven't already been added, I'm also leaning towards some kind of race condition here..

Have we seen this in other PRs?

So, we add some $time? We don't have to be 0sec.

Either way, maybe github support should be notified about this?

Also AFAIK checking labels first shouldn't even be necessary since github only adds the complement of the intersection of the old label set and the new label set (it does not remove existing labels).

@mscdex you want to do the honors?

@jbergstroem I can try, but I don't have any contacts at Github.

As the bot fetches the existing labels on a PR via the github API, before adding new ones which haven't already been added ...

I stand corrected -- just realised we don't check existing labels anymore, as of last week w/4b6f2b3. The newest version of node-github got a new API letting us add labels which POSTs to api.github.com/repos/nodejs/node/issues/X/labels

@mscdex I've had pretty good success with their public support (https://github.com/contact) -- just ref this issue.

@mscdex keep us updated. I've see this on several PRs lately, and if GH is too busy to have a look at this, it's trivial for us revert and only add labels which haven't already been added.

Just got a response from Github, they've now opened an issue internally to investigate this further. They can't promise an ETA but will keep me updated.

FYI I've just contacted GitHub support about this again.

Still no progress on this internally at GitHub, and no estimate on when it will be prioritised.

In other words, we'll have to get a work around in place to avoid this happening in the near future.