Permalink
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
23 lines (14 sloc) 1 KB

Contributing

We love pull requests from everyone.

Install the development environment

  • Follow the installation instructions in our wiki.

Create a Pull Request

  1. Fork the repository: https://help.github.com/articles/fork-a-repo
  2. Create a branch in your fork: https://help.github.com/articles/creating-and-deleting-branches-within-your-repository
  3. Pull the branch as a pull request targeting omichel:webots@master: https://help.github.com/articles/creating-a-pull-request-from-a-fork
  4. Wait for our unit tests and review of your pull request.

Our git workflow is explained in detail here.

Development Guideline

  • Follow our Coding Style.
  • Avoid comitting files that exist elsewhere. Instead we should link to the source of these files.
  • Avoid comitting files that can be re-created from other files using a Makefile, a script or a compiler.