Creating a release

The following steps have to be followed to create a release:

1. Update the changelog file
2. commit all changes
3. Do a git push: git push
4. Create a git tag in the format v+VERSION (eg. v7.0.0): git tag vVERSION
5. Push tags: git push --tags

In case of a mistake, the tag can be deleted:

1. Locally: git tag -d vVERSION
2. Remotely: git push --delete origin vVERSION