[petsc-dev] Bogus tag

[Balay, Satish]

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 <petsc-dev at mcs.anl.gov> writes:
> 
> > $ git branch
> > * master
> >
> > $ git describe
> > WIP-112-g872c329e82
> >
> > $ git show WIP
> > tag WIP
> > Tagger: Jed Brown <jed at 59a2.org>
> > 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/
>