PR reported as open but is merged
JulienPalard opened this issue · 2 comments
JulienPalard commented
In this issue : https://bugs.python.org/issue35579 PR 11323 is reported as open but is merged.
terryjreedy commented
I have seen status change as much as a day later, or never. When closing, I may note on the issue that a PR is really closed. In this case, hitting [edit] shows that is was changed from open to merged and 10 minutes later back to open.
2018-12-26 15:03:47 miss-islington set status: merged -> open
2018-12-26 14:53:05 miss-islington set status: open -> merged
The reversion happened at the same minute as one of the duplicate reports.
ezio-melotti commented
We now migrated to GitHub, so this can be closed.