removing `after-port`?

Stream: mathlib4

[Jireh Loreaux]

Now that we have cut the port-complete tags, there is no purpose for the after-port tags in mathlib4, right? Should we obliterate that tag?

[Yury G. Kudryashov]

@Eric Wieser :up:

[Scott Morrison]

I think so!

[Jireh Loreaux]

Oh, I guess the same goes for new-feature.

[Scott Morrison]

I removed after-port.

[Scott Morrison]

I think we can also remove new-feature safely, it seems to bear no weight. Objections?

[Eric Wieser]

The one argument for keeping it is that it still records info about PRs that were already merged