Re-opening PRs

[Aleksey Shipilev]

On 3/5/21 2:44 PM, Robin Westberg wrote:
> I guess the only solution other than opening a new one would be to get an admin to reopen the PR.
> I’m fairly certain that it has been possible for regular users to reopen PRs in the past, so it
> is possible that something has changed on the GitHub side.. But as it stands, it certainly is a
> bit inconvenient. So my suggestion is that I reopen PR #1343 and disable automatic closing of PRs
> for now.

Yeah, it would be nice to tame the autoclosing bot a bit, until this is resolved.

-- 
Thanks,
-Aleksey