Thanks! I'll create an account on gitter soon then.
Some follow up questions:
Should our name be added to the file copyright headers when changing existing files?
If yes, does that apply for minor changes aswell, or where is the limit?
- Fixing a bug on one line?
- Changing documentation?
- Deleting unwanted stuff? (technically, nothing original is added in this case, but content is changed).
I couldn't find any routines on how to actually do the pull request and I'm new to github. I think I have the basic idea of it, but is this the following the correct way?
1. make a fork on github and check it out locally (fork from the development version?).
2. make a branch for the change (is there a naming standard for the branches somewhere to read?)
3. Make neccessary changes, commit it. (same here, any guidelines for commit comments that I should know of?)
4. Push to github
5. Make a pull request using the new branch
Good so far or did I get something wrong/miss any steps?