CI

Notes on github actions.

See https://docs.github.com/en/actions/learn-github-actions/variables#default-environment-variables for environment variables set by github. (Default values seem to have been removed from the page)