Developer workflow: Making changes

This is internal information for the developers on this project.

How to make changes

Create a feature branch off of the "develop" branch

git checkout develop
git pull
git branch feature/mytopic

Make the modifications in one or several logically separated commits.
Push the commits to Github with git push.
Create a pull request (PR) on Github for the feature branch against the develop branch, and optionally select reviewers. Emails about the PR and about reviewing will automatically be sent by Github.
If the PR refers to an issue, consider referring to the issue in the PR's comment. Github will automatically link to the correct issue if you include a string like in issue #NNN, and it will additionally annotate this in the mentioned issue automatically.

Alternatively, refer to the PR in a comment in the issue with in PR #NNN.

In both variations, it's the hash (#) followed by a number that triggers the association.
Whomever reviews the PR will accept or reject the PR (with comments). If the PR is accepted, the reviewer will perform the merge immediately. The reviewer will also remove the feature branch on Github.

If the PR is rejected, further changes are committed and pushed to the same feature branch, until the PR is acceptable.

Emails will be sent automatically by Github about the various actions mentioned above.
Once the PR has been merged, the local feature branch may optionally be deleted.
```
git checkout develop
git branch -D feature/mytopic
```