Add settings.json linter documentation

[shitchell]

Add a JSON example of how to enable linting in settings.json

[shitchell]

As mentioned in #3366, I spent months trying to figure out how to get linting working. I definitely referenced the documentation, but there wasn't any clear documentation on how to set it up (via "linter": true in settings.json). This isn't to criticize, just to point out that some fools like myself might benefit from a little spoon-feeding in the linter readme :)

[Andriamanitra]

I would also mention the set linter on|off command which is the easier way to do this.

[Andriamanitra]

This is already documented in help options: https://github.com/zyedidia/micro/blob/dc7759204bd9af8ed7d8acfd340a367ec3cfbf74/runtime/help/options.md?plain=1#L465-L486

I guess it doesn't hurt to repeat the same thing in the plugins own help file, but should we then add it to the help for the other built-in plugins too? It is also worth mentioning that linter is enabled by default when the "linter" key is absent from settings.json.

[shitchell]

This is already documented in help options:

https://github.com/zyedidia/micro/blob/dc7759204bd9af8ed7d8acfd340a367ec3cfbf74/runtime/help/options.md?plain=1#L465-L486

I guess it doesn't hurt to repeat the same thing in the plugins own help file, but should we then add it to the help for the other built-in plugins too? It is also worth mentioning that linter is enabled by default when the "linter" key is absent from settings.json.

I saw that, but the way I read it was more of these plugins with these names are available, and they each have some undisclosed setting name to enable/disable them. Especially since each key is followed by a description, that read more like a list of plugin names and descriptions than keys that go in the settings.json file.

There is also a sample settings.json file provided that includes the "linter" setting, but I simply didn't see it in the list. That could be me being blind, and perhaps most people are more observant than me lol, and if so then it might be unnecessarily redundant to add here as well. I do think having it in the linter docs would've saved me, though :P

It is also worth mentioning that linter is enabled by default when the "linter" key is absent from settings.json.

That just makes me feel even more braindead... I probably copied all the settings to my settings.json (as reference for what all the options are), manually set that one to false for some reason, and then forgot about it. Probably ~2 years ago. And I share my configs across devices, so it wasn't working on anything... 🤦

but should we then add it to the help for the other built-in plugins too?

If that makes this addition make more sense, I'd be happy to do that :) Or if others feel this is indeed unnecessary redundancy, that's fair, too 😛