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?
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.)
the order is open then rebase
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?
It looks like reopening still works.
I would not have expected that from your comment, so maybe something has changed on GitHub.
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?
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).
To reopen you need to match the hash, but indeed that's a PITA
Last updated: Nov 29 2023 at 18:01 UTC