A post-modern development environment.

release docs: Fix `git push` command for the release tag master

Git can be configured to push tags with `push.followTags` but this is not the default. Pushing the tag explicitly with `git push <remote> <tag>` is generally considered safer anyways since it only attempts to push the desired tag.


+1 -1
1 changed file