Stream: Coq devs & plugin devs

Topic: GitHub edit button


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:46):

Yes, I have just realised

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:46):

Sorry about that

view this post on Zulip Théo Zimmermann (Jul 09 2021 at 10:46):

I've deleted your branch FYI.

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:46):

Thanks, whats the correct way to do that?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:47):

I misunderstood where github was creating the branch

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 09 2021 at 10:48):

Sure I can do this fix.

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:48):

Sorry about the mess, I'll be more careful next time :-)

view this post on Zulip Théo Zimmermann (Jul 09 2021 at 10:48):

No worries, everyone has been hit by this misfeature.

view this post on Zulip Théo Zimmermann (Jul 09 2021 at 10:50):

Done https://github.com/coq/coq/pull/14623


Last updated: Oct 21 2021 at 21:03 UTC