Xavier Morel bf34e9aa95 [FIX] runbot_merge: ensure PR description is correct on merge ... Because sometimes github updates are missed (usually because github never triggers it), it's possible for the mergebot's view of a PR description to be incorrect. In that case, the PR may get merged with the wrong merge message entirely, through no fault of the user. Since we already fetch the PR info when staging it, there's very little overhead to checking that the PR message we store is correct then, and update it if it's not. This means the forward-port's description should also be correct. While at it, clean the forward port PR's creation a bit: - there should always be a message since the title is required on PRs (only the body can be missing), therefore no need to check that - as we're adding a bunch of pseudo-headers, there always is a body, no need for the condition - inline the `pr_data` and `URL`: they were extracted for the support of draft PRs, since that's been removed it's now unnecessary Fixes #530		2021-09-24 15:18:36 +02:00
..
__init__.py	[ADD] runbot_merge: a merge bot	2018-09-03 13:16:36 +02:00
pull_requests.py	[FIX] runbot_merge: ensure PR description is correct on merge	2021-09-24 15:18:36 +02:00
res_partner.py	[IMP] runbot_merge: overridable CI	2020-11-20 07:41:54 +01:00