* When you merge a PR through the UI it can happen that the commit is
merged, _without _the PR being closed!
On 20/06/2019 11:21, Chesnay Schepler wrote:
Attention fellow committers,
There is currently an issue with GitHub where it may not be possible
to close PRs or comment on them.
When you merge a PR through the UI it can happen that the commit is
merged, with the PR being closed! When this happens, don't try to
merge it again (like I did....) or we'll end up with empty commits
like
https://github.com/apache/flink/commit/c5ff8e3c1040260df9dcf3f5278d5409c4077a2e
.
GitHub is aware of this issue, see https://www.githubstatus.com/
