+0
−43
Loading
This reverts commit 402b41c1. GitHub' API repeatedly returns wrong data which causes closed PRs when the changes had not been merged, yet. We have closed a bit more than 100 PRs overall, most of them initially - the feature is not really that important overall.