3
$\begingroup$

I've just created a question and tried to add a tag "cubical-type-theory", but my keyboard is problematic and causes the tag to be "cubical--type-theory" (with an unexpected -).

I want to do a rename, but when I try to remove the old tag and add the correct-spelling one, the website says I need to raise this on meta site. This is what I'm doing here. What should I do to get it renamed (or is it proper to leave it there?)?

$\endgroup$
  • $\begingroup$ Link to the question: cs.stackexchange.com/q/103146/79971 $\endgroup$ – ice1000 Jan 20 at 19:36
  • $\begingroup$ General tagging advice: try to use existing tags are much as possible; it makes your question more findable and connects it with other related questions. I notice that you created rather specific tags but didn't use the overarching type-theory. $\endgroup$ – Raphael Jan 20 at 21:10
  • $\begingroup$ @Raphael Because I think it's very very specific to Cubical Type Theory. Thanks for the advice, I'll keep in mind. $\endgroup$ – ice1000 Jan 21 at 0:18
3
$\begingroup$

There's very little to worry about here: just create the new, correct tag. The old one, if unused, will be cleaned up by the system after a while. (I went ahead and fixed the spelling.)

If there are multiple legitimate spellings or variants, you can propose synonyms.

$\endgroup$
6
$\begingroup$

Normally, if you've just created a tag, you can rename it by editing the question(s) that have it to remove the misspelled tag name and adding the correct tag name. There's no way to explicitly delete the old tag name, but once a tag is not present on any question, it will disappear after a day or so (there's a daily cleanup job).

If the tag is already present on many questions, that would be a different matter requiring a meta discussion. If the outcome of the discussion is to rename the tag, moderators have a tag renaming tool that doesn't bump questions.

There's an exception: if the old name and the new name differ only in the placement of hyphens or in a final s, the system will prevent you from creating the new name. This is because of a general rule that prevents having two tags that differ only in the placement of hyphens or a tag that looks like the plural of another. That's why you were referred to meta. In this case (missing hyphen, misplaced hyphen, extra hyphen), since the fix is clear and doesn't need community discussion, you can flag and ask a moderator to do the renaming.

$\endgroup$
  • $\begingroup$ No, the tag names are too similar to get a rename. The website says that there's already a cubical--type-theory so I can't use cubical-type-theory. Otherwise I may just do the rename and ask a different question about how to remove the old one... $\endgroup$ – ice1000 Jan 21 at 23:26
  • $\begingroup$ @ice1000 Yes, the tag names are too similar, that's what I explain in the third paragraph. $\endgroup$ – Gilles Jan 22 at 5:53
  • $\begingroup$ Interesting; for me, the renaming in that question's tag editor just worked, without any notice that I was doing something special. Good to know that I was using mod powers! $\endgroup$ – Raphael Jan 22 at 16:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .