Vladimir Panteleev

> Pull-Request: The pull request number should always be on the first line. (This wasn't the case when the other merge methods were first introduced.) > Pull-Request-Title: The first line...

What's the status of this considering that we now use our own Bugzilla integration?

Is this still relevant today, now that we have staff reviewing PRs? > Moving such PRs to a hold zone where they don't clutter development could be an interesting experiment....

Should we just include a list of commits and their commit messages in the merge commit message, then?

For the WIP case I understand it's no longer relevant as GitHub now has draft PRs. What other commands could the bot understand?

I think at this point it would be simpler to store locally which commit SHA1s belong to which PRs (when a PR is created or synchronized).

Another instance: https://github.com/dlang/dmd/pull/12592

I think due to the way sharding is implemented, sometimes the request to create a resource go to one server, and an immediately following request to enumerate said resource goes...

So as discussed on Slack, this seems to have fallen off at some point. I got it working again, though, it seems to take a very long time to run....

> I got it working again, though, it seems to take a very long time to run. Figured it out, it was getting stuck in an infinite loop because it...