Advanced

Updating the git versions and releases

To list the git version tags:

git tag -l

To list the git version tags along with a brief 1-line description (-n<K> for K lines):

git tag -l -n1

To add a tag use:

git tag -a <vX.Y.Z> -m "<SOME BRIEF MESSAGE>"

The tag then needs to be pushed:

git push --tags

To set a release with a tag:

gh release create $(git describe --tags --abbrev=0)

Updating the remote documentation.

To update the documentation hosted remotely (e.g. on GitHub Pages), then on master we need to redeploy the documents after the most relevant commit by calling:

mkdocs gh-deploy --clean

---

Last update: September 12, 2023
Created: July 23, 2023