How to rename a git tag

Here is how I rename a tag old to new:
```
git tag new old
git tag -d old
git push origin :refs/tags/old
git push --tags
```
Finally, make sure that the other users remove the deleted tag. Please tell them (co-workers) to run the following command:

```
git pull --prune --tags
```

Daniel Gomonea
15 Jun 2020