When bors merges a pull request, it changes the title to [Merged by Bors] - <original title>. I'm not interested in this feature, and think it's a good idea to make it configurable. Is that possible in a way that I missed in the documentation?
That should only happen if squash mode is turned on, in which case, it's the only way to distinguish between merged pull requests and closed ones. Why would you want to get rid of that?
2 Likes
Yes, we use squash mode. I only just realized that the PR doesn't really get merged, but closed by bors. This actually makes this feature valuable. I actually wish there was a way to tell Github that the PR is merged and not closed, but I assume it's not technically possible, so 
.
Sorry for being trigger happy on opening this issue.
I think there is a side effect of changing PR title is that Gmail (and other mail clients) thinks it should be a new thread instead of attaching it to the previous email thread. We have developers found it confusing when a new email thread is created. Any suggestion to solve this problem?
Thanks
One thing I could think of is that we could use something like a tag Merged by bors instead of changing the PR title.
Maybe change the PR title after closing the PR and leaving a comment? That way, no emails actually get sent with the new title.
It seems that changing the title after adding the comment and closing the PR is a no brainer.
Optionally adding a label instead of changing the title (user preference) seems like a good idea to me, as well, if it’s not too hard to implement.
Marking the PR as merged would be ideal, but unfortunately it doesn’t look like Github is exposing this functionality.
I created a PR for changing the order of adding comments and closing the PR.
@notriddle I was bugged by this question today and spent a while before found an answer.
I believe it should be in the docs.