Bors' merge commit drops title from original PR

[pnkfelix]

When Bors does the merge of the PR, it only puts the description from the PR into its commit message on the merge commit. Importantly, it leaves out the original title, which I claim is a bug in Bors.

This bug matters because the workflow of github often leads one to put important info into the title of the PR and the title alone: When I create a PR via github (on the button that comes up when you've recently pushed to a branch on your fork of the repository), it extracts the title of the PR from the first line of the commit message (or some prefix of that first line), and then uses the rest of the commit message as the description, leaving out the first sentence itself.

---

Concrete example:

Consider this PR: rust-lang/rust#12154

Here is the commit that the title and description of that PR was based upon: pnkfelix/rust@d2d1129

But here is the merge commit that bors decided to create: rust-lang/rust@fd4979a

Notably, the first line of the original commit had the most important information about the commit, but it is missing from bors' merge.

---

Now, this is not a fatal bug, because:

1. One can easily workaround it by copying the title into the description in the PR (or, if one prefers, formatting one's git commits with a title followed by a description that stands indpendently from the title).
2. One can always follow the parents of the bors-merge in the commit graph to find the original commit's first line so no information has been lost.

But it would still be nice if Bors just copied the title into the commit message for the merge.

[Vagabond]

This was fixed in c763fc3

Bors merge commits now are the same as are generated by hitting the merge button on a PR (with an additional Reviewed-By line). You can see an example here: basho/riak_cs@d0b8275

I think we can close this now?

[pnkfelix]

\o/

[pnkfelix]

@brson I don't think our current version of bors that we use in rust has this fix incorporated?

See e.g. this recent commit: rust-lang/rust@6e7f170 versus its originating PR: rust-lang/rust#12665

[pnkfelix]

@Vagabond looking at your example basho/riak_cs@d0b8275 , is your version of bors now including the title but cutting out the description that follows the title (which in the case of basho/riak_cs@d0b8275 it seems like you would have "@slfritchie, can you please double-check 6014262?" in the commit as well if it copied title and description into bors' merge?)

[Vagabond]

As far as I can tell, github merge commits (generated when you click the merge button) do not include the PR body, just the title.

[pnkfelix]

@brson hey huon tells me you held off on a bors upgrade until after the work week, so I just wanted to ping again about this.