Open aisejohan opened 6 years ago
The proposal involved systematically recording this information in the tags file.
Right! OK, so in the tags file on the line corresponding to the deleted tag I could make it look like this
#00EL,algebra-equation-idempotent-exact-sequence This equation was in a second proof 00EE which we removed in commit 623aef2b
or
#00DU,algebra-lemma-localize-colimit Taken out as an exact duplicate of 00CR
Somehow retaining the latex label that used to be there seems appropriate. When I get this done (at some future time), I will let you know.
Very low priority. If a visitor requests a page corresponding to an inactive tag we could/should have a message explaining what happened. I seem to remember @pbelmans suggesting a mechanism for doing this, but I can't recall the exact proposal.