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.
This prepares a PR with updated history and version
for auto-merge. Any new PRs are merged into HISTORY.md
but existing entries are left untouched. Thus, we can
tweak wording in HISTORY.md at any time without the
effort of figuring out which PRs need to be present
manually.
