Merge branch 'develop' into align_userdata

This commit is contained in:
Matthias
2019-08-01 19:33:45 +02:00
13 changed files with 160 additions and 116 deletions

View File

@@ -12,8 +12,8 @@ Special fields for the documentation (like Note boxes, ...) can be found [here](
## Developer setup
To configure a development environment, use best use the `setup.sh` script and answer "y" when asked "Do you want to install dependencies for dev [y/N]? ".
Alternatively (if your system is not supported by the setup.sh script), follow the manual installation process and run `pip3 install -r requirements-dev.txt`.
To configure a development environment, best use the `setup.sh` script and answer "y" when asked "Do you want to install dependencies for dev [y/N]? ".
Alternatively (if your system is not supported by the setup.sh script), follow the manual installation process and run `pip3 install -e .[all]`.
This will install all required tools for development, including `pytest`, `flake8`, `mypy`, and `coveralls`.
@@ -156,6 +156,8 @@ git log --oneline --no-decorate --no-merges master..develop
### Create github release / tag
Once the PR against master is merged (best right after merging):
* Use the button "Draft a new release" in the Github UI (subsection releases)
* Use the version-number specified as tag.
* Use "master" as reference (this step comes after the above PR is merged).