Skip to content

Commit

Permalink
fix(docs/howto-contribute): main repository has moved
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Feb 26, 2019
1 parent 7450cc5 commit 3f47739
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions docs/howto-contribute.md
Expand Up @@ -7,20 +7,17 @@ for a good introduction.
Here are some tips and tricks
to make the process of contributing as smooth as possible.

1. Use Zulip: https://leanprover.zulipchat.com/#
1. Use Zulip: https://leanprover.zulipchat.com/
Discuss your contribution while you are working on it.
2. Adhere to the guidelines:
- The [style guide](/docs/style.md) for contributors.
- The explanation of [naming conventions](/docs/naming.md).
- The [git commit conventions](https://github.com/leanprover/lean/blob/master/doc/commit_convention.md).
3. Create a pull request from a feature branch on your personal fork,
as explained in the link above.
as explained in the link above, or from a branch of the main repository if you have commit access (you can ask for access on Zulip).


## The community fork and the nursery

The community also uses https://github.com/leanprover-community/mathlib
for collaborative contributions: ask on Zulip if you'd like commit access.
## The nursery

Finally, https://github.com/leanprover-community/mathlib-nursery
makes it possible to have early access to work in progress.
Expand Down

0 comments on commit 3f47739

Please sign in to comment.