[m-rev.] diff: fix a bug in tools/import_srcdist

[Peter Wang]

On Thu, 27 Jan 2022 14:49:20 +1100 Julien Fischer <jfischer at opturion.com> wrote:
> 
> Hi Peter,
> 
> On Thu, 27 Jan 2022, Peter Wang wrote:
> 
> >> I assume you can modify the script you have below to delete the
> >> broken tags?
> >
> > I've reimported 141 archives into my workspace.
> > Do you want me to force-push the fixed tags now?
> 
> Yes.
> 
> > That leaves the following 176 tags witih missing files.
> > Do you want me to delete those tags now?
> 
> Yes, go ahead.
> 
> Thanks for that.

Ok, done. Looks like you will want to run something like:

    git fetch origin --prune --prune-tags

to remove the stale tags from your workspace.

Peter