Thanks for the reminder! @Chesnay Schepler
I thought I had a network problem, it turned out to be a GitHub problem.
I can't comment on the PR 5 minutes ago, it should be OK now！
Chesnay Schepler 于2019年6月20日周四 下午5:21写道：
> Attention fellow committers,
>
> There is currently an issue with GitHub
* 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 y
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.
