Commented-out pull-request template ends up in commit messages for merges

[joshtriplett]

Now that we have a PR template, submitting a pull request (either via the web form or via gh pr create) will commonly end up with a commented-out version of the pull request template in the message. This doesn't get rendered in the GitHub web UI, but when bors does a merge, it includes the entire PR template in the commit message for the merge. See dc6d847 for instance.

[weihanglo]

That's not good 😞
Just curious. Does #10258 contain that PR template in it's description body?

[joshtriplett]

@weihanglo Yes, it does, within HTML comments.

[alexcrichton]

Oh I think this is a bors-ism, I believe GitHub strips out the comment when you hit the merge button. Alas though :(

[Mark-Simulacrum]

There's already some similar-looking support in bors for cutting text from PR bodies (https://github.com/rust-lang/homu/blob/cf0674989a2b8be2c6c86e344f5cf1cb9320d049/homu/main.py#L46-L50) -- maybe possible to either use that syntax or a fairly easy patch to add some more human-readable header there.

[joshtriplett]

@Mark-Simulacrum Ah, that looks like it should work. I'll send in a PR adding that to the PR template.

[joshtriplett]

#10267

[weihanglo]

I believe this is resolved by #10267. Closing.