@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.
Indeed, GitHub will then create a branch on the main repo instead of in your fork.
Yes, I have just realised
Sorry about that
I've deleted your branch FYI.
Thanks, whats the correct way to do that?
Or could you do it, I just added a .md to the INSTALL.md link in /dev/doc/README.md
I misunderstood where github was creating the branch
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.
Sure I can do this fix.
Sorry about the mess, I'll be more careful next time :-)
No worries, everyone has been hit by this misfeature.
Last updated: Oct 21 2021 at 21:03 UTC