Well this also requires: - everyone who pulled this tag to manually delete it from their local clone.
I don't know if there is a good way to do this. There is 'git fetch --prune-tags' - but its not useful if you keep local tags [that you don't intend to push out] - and prevent folks from re-pushing this tag (from a clone where this tag is not deleted) [I've setup branch permissions at bitbucket to help with this] Satish On Fri, 3 May 2019, Jed Brown via petsc-dev wrote: > Gross. I deleted it. > > That was created when I was trying to label a PR in the web interface. > It didn't work as intended, but I didn't realize it had left behind a > Git tag in the repository. > > Lisandro Dalcin via petsc-dev <[email protected]> writes: > > > $ git branch > > * master > > > > $ git describe > > WIP-112-g872c329e82 > > > > $ git show WIP > > tag WIP > > Tagger: Jed Brown <[email protected]> > > Date: Wed Apr 24 22:56:11 2019 +0000 > > > > Work In Progress (do not merge) > > ... > > > > Is there any way we can get rid of that? > > > > -- > > Lisandro Dalcin > > ============ > > Research Scientist > > Extreme Computing Research Center (ECRC) > > King Abdullah University of Science and Technology (KAUST) > > http://ecrc.kaust.edu.sa/ >
