Marc Durdin d8f81cbdf1 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.		2022-05-17 10:43:07 +10:00
..
queries.ts	chore(common): improve PR reporting of changes	2022-05-17 10:43:07 +10:00