Merge branch 'master' into develop

The develop branch was missing several commits according to GitHub,
despite git diff between the two branches showing no code differences.

This brings develop in sync with master, other than the next minor
release placeholder being present in develop's CHANGELOG.