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/
