Commit d8f81cbd authored by Marc Durdin's avatar Marc Durdin
Browse files

chore(common): improve PR reporting of changes

Fixes #6391.

The issue here was quite nuanced: where we merged a PR, and then merged
the changes into an earlier PR, but left it open, the earlier PR could
end up getting the release information comment from keyman-server
instead of the later, merged PR. This was because the commit would
appear in both PRs, so GitHub would report on both of them.

This is not a 100% fix -- but it should stop the PR tagging on unmerged
pull requests. The one situation where this may leave a gap is where we
have multiple PRs merged on the same day, where a later PR's changes are
merged into an earlier PR; in this case I think it is possible that one
of the PRs will not get the informative version comment.

But given the current fix should avoid the more common situation, I am
comfortable to leave it as is for now. This is only informative data...
and a more complete fix is a distraction.
parent cf276114
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment