Stream: helpdesk (published)

Topic: close PR on public registry

Filippos Christou (Mar 14 2023 at 16:27):

How can I close this PR on the public registry ?

Mosè Giordano (Mar 15 2023 at 00:48):

As a general recommendation, leave a comment in the PR asking for it to be closed. Maybe a maintainer will see and close it, in any case all PRs inactive for over a month are closed automatically (if they hadn't been merged, it usually means that the submitter had to do something else anyway)

Last updated: Oct 02 2023 at 04:34 UTC