Hi all
Marc recently noticed that some tags in Git repository were wrong. I hopefully reviewed and fixed them all and the tags should be correct now. As the old tags are not automatically update when you do simple pull, please update your local copy of tags using:
git pull --tags