max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(.github/CONTRIBUTING): fix typos and URLs

Browse source
This commit is contained in:
Sebastian Ullrich 2017-10-30 16:23:22 +01:00 • committed by GitHub
parent da1fc03d15
commit 853b0f7648
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
.github/CONTRIBUTING.md vendored
View file

@ -1,15 +1,15 @@
# Contributing to Lean
Thank you for choosing to contribute to Lean, this document is a intended as a brief guide
Thank you for choosing to contribute to Lean. This document is intended as a brief guide
for new contributors to help streamline the process and make it as easy as possible
for you (the contributors) and us (the maintainers).
### Writing Code
- [Coding Style](doc/coding_style.md)
- [Library Style Conventions](doc/lean/library_style.org)
- [Git Commit Conventions](doc/commit_convention.md)
- [Automatic Builds](doc/make/travis.md)
- [Coding Style](../doc/coding_style.md)
- [Library Style Conventions](../doc/lean/library_style.org)
- [Git Commit Conventions](../doc/commit_convention.md)
- [Automatic Builds](../doc/make/travis.md)
# Opening Issues
@ -27,7 +27,7 @@ So, here are some guidelines for submitting PRs:
- Small bug fixes are always welcome.
- Before implementing a major feature or refactoring the code, please ask whether the change is welcome or not.
The worst kind of PR is the "unwanted one". That is, we don’t want it, but we have to explain why we will not merge it.
- Ensure all test suite works before submitting a PR. You can run the test suite (after building Lean and the Lean library) by calling `ctest` in your build directory.
- Ensure all tests work before submitting a PR. You can run the test suite (after building Lean and the Lean library) by calling `ctest` in your build directory.
- Ensure your Pull Request meets the coding and commit conventions documented above.
- Ensure your Pull Request contains tests for the behavior, for both features or
bug fixes.