We should add some developer documentation about how to cut new tags of this repo, especially since the default recommendation is to move tags, which is probably pretty counter-intuitive for most developers.