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/
