Stream: helpdesk (published)

Topic: close PR on public registry


view this post on Zulip Filippos Christou (Mar 14 2023 at 16:27):

How can I close this PR on the public registry ?

view this post on Zulip 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: Nov 22 2024 at 04:41 UTC