Merge-conflict bot broken?

Stream: mathlib4

[Robin Carlier]

I have been getting several false positive by the merge-conflict bot today (e.g in #25545), sometimes, removing the merge conflict tag could not be achieved by just merging master on the PR, but I also had to merge master in the dependent PRs.
When the tag was added, the post-or-update-summary-comment had a weird output in its "update merge-conflict label" runs, see e.g here, or here in an other PR. It seems a runner has a misconfigured git and it causes troubles.
cc @Bryan Gin-ge Chen

[Jovan Gerbscheid]

I've got the same at #25534. There is no merge conflict, but I'm getting the merge-conflict tag.

[Robin Carlier]

Also in #25548...

[Eric Wieser]

I would guess this is a git behavior change?

[Bryan Gin-ge Chen]

Apologies for the annoyance, everyone. There is an issue in the PR summary bot which hopefully #25547 will address.

[Robin Carlier]

Eric Wieser said:

I would guess this is a git behavior change?

I would be very surprised if that's the case. I think git developers have a strong policy about not introducing breaking changes in behaviour, and suddenly deciding to throw an error on something that did not used to seems unlikely.

[Damiano Testa]

What I thought was a patch for this issue has been merged: has anyone observed further weird behaviour with merge-conflict?

[Ruben Van de Velde]

It seems like #30639 didn't get a merge-conflict label automatically, does anyone want to figure out why?

[Bryan Gin-ge Chen]

My best guess is that the merge conflict bot ran out of tokens before it got to that PR. I think it eventually cycles through all the PRs but it might take a quite a while now.