Zulip Chat Archive

Stream: new members

Topic: Removing forking as an option "How to Contribute"

Hunter Monroe (Nov 22 2023 at 22:22):

Can I delete from "How to Contribute" the part about forking being an option? I tried that making a small change to a comment, and it would not build after doing a pull request to mathlib4. The normal way of making a branch worked immediately. So I would delete this: "Otherwise, you'll need to go to https://github.com/leanprover-community/mathlib4 and click "Fork" in the top right, to make your own fork of the repository." I can see how someone waiting for permission to branch might want to create a fork in the interim but not to do a pull request except from a branch.

Last updated: Dec 20 2023 at 11:08 UTC