Théo Zimmermann (Jul 09 2021 at 10:46): Théo Zimmermann (Jul 09 2021 at 10:46):@Ali Caglayan Now that you have write access to the Coq repository, you cannot anymore use the edit button from GitHub as easily as before.
Théo Zimmermann (Jul 09 2021 at 10:46):Indeed, GitHub will then create a branch on the main repo instead of in your fork.
Ali Caglayan (Jul 09 2021 at 10:46):Yes, I have just realised
Ali Caglayan (Jul 09 2021 at 10:46):Sorry about that
Théo Zimmermann (Jul 09 2021 at 10:46):I've deleted your branch FYI.
Ali Caglayan (Jul 09 2021 at 10:46):Thanks, whats the correct way to do that?
Ali Caglayan (Jul 09 2021 at 10:47):Or could you do it, I just added a .md to the INSTALL.md link in /dev/doc/README.md
Ali Caglayan (Jul 09 2021 at 10:47):I misunderstood where github was creating the branch
Théo Zimmermann (Jul 09 2021 at 10:48):If you want to use the edit button in the web, what you can do is go to the masterbranch in your fork, make sure it is up-to-date (there's a GitHub button to synchronize) and then follow the same process as before. That's way more complex unfortunately.
Théo Zimmermann (Jul 09 2021 at 10:48):Sure I can do this fix.
Ali Caglayan (Jul 09 2021 at 10:48):Sorry about the mess, I'll be more careful next time :-)
Théo Zimmermann (Jul 09 2021 at 10:48):No worries, everyone has been hit by this misfeature.
Théo Zimmermann (Jul 09 2021 at 10:50):Done https://github.com/coq/coq/pull/14623
Last updated: Sep 25 2023 at 14:01 UTC