Do we need to track duplicated plugin descriptions in `options.md` & `plugins.md`?

[JoeKar]

Do we really need to track the same description twice? https://github.com/zyedidia/micro/blob/838f371486ab3a083cee2471d8ee7f1f33acd595/runtime/help/options.md?plain=1#L471-L481 https://github.com/zyedidia/micro/blob/838f371486ab3a083cee2471d8ee7f1f33acd595/runtime/help/plugins.md?plain=1#L416-L426

I would prefer to track it in one file only and since they are related to plugins the plugins.md would fit the most.

There are already votes against the removal:

I think these should be kept because someone who is autocompleting set could try to search for them in options.md to figure out what they mean. It's not immediately obvious (partly due to unfortunate naming of the plugins) that they should be looking at plugins.md instead.