"Balay, Satish" <[email protected]> writes: > Well this also requires: > > - everyone who pulled this tag to manually delete it from their local clone.
I think the automatically pushing tags issue was resolved a while ago in Git defaults. > 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/ >>
