Thierry Martinez (Oct 07 2022 at 13:14): 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?
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.)
Gaëtan Gilbert (Oct 07 2022 at 13:17):the order is open then rebase
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?
Théo Zimmermann (Oct 07 2022 at 13:24):It looks like reopening still works.
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.
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?
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).
Thierry Martinez (Oct 07 2022 at 13:30):Many thanks!
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: Nov 29 2023 at 18:01 UTC