Stream: Coq devs & plugin devs

Topic: Reopen closed PR on GitHub


view this post on Zulip Thierry Martinez (Oct 07 2022 at 13:14):

PR https://github.com/coq/coq/pull/16097 has been closed because I did not rebase on time. Can I reopen it and rebase, or should I open another PR?

view this post on Zulip Guillaume Melquiond (Oct 07 2022 at 13:15):

You can (and should) reuse the same PR, but you have to perform the steps in a very specific order so as to please Github. (I don't remember what it was though.)

view this post on Zulip Gaëtan Gilbert (Oct 07 2022 at 13:17):

the order is open then rebase

view this post on Zulip Thierry Martinez (Oct 07 2022 at 13:22):

Thanks! I am afraid I have pushed to soon on my branch (before reopening the PR). I see at the end of the PR: _Closed with unmerged commits_ . Yet, I restored the branch to the same state than the PR (both PR and branch points to commit 1358fb8). Is there something I can do to reopen the PR or is it too late?

view this post on Zulip Théo Zimmermann (Oct 07 2022 at 13:24):

It looks like reopening still works.

view this post on Zulip Théo Zimmermann (Oct 07 2022 at 13:25):

I would not have expected that from your comment, so maybe something has changed on GitHub.

view this post on Zulip Thierry Martinez (Oct 07 2022 at 13:26):

Ok, thank you very much, Théo! I did not see any “Open” button, perhaps only a “maintainer” (or some other special role) can do that?

view this post on Zulip Théo Zimmermann (Oct 07 2022 at 13:29):

Hum, that's possible. I've invited you to join the @coq/contributors team so that you have more permissions on the Coq repository (like opening/closing issues/PRs and adding labels).

view this post on Zulip Thierry Martinez (Oct 07 2022 at 13:30):

Many thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 14:04):

To reopen you need to match the hash, but indeed that's a PITA


Last updated: Feb 06 2023 at 19:03 UTC