On Sat, Jan 9, 2016 at 11:16 AM, Japheth Cleaver <cleaver(a)terabithia.org>
If no release tags are ever made, that's one thing... but it
feels like if
a release tag is present we should be using that.
Correct... that is clearly spelled out in the guideline under the Commit
Revision section. GIT TAGS have already been discussed ad infinitum.
Changing of GIT TAGS after a push is considered "insane" behavior - and if
you have a developer who is doing that, you have bigger issues to consider
- such as what other crap are they doing.