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:

micro/runtime/help/options.md

Lines 465 to 486 in dc77592

	Plugin options: all plugins come with a special option to enable or disable
	them. The option is a boolean with the same name as the plugin itself.
	By default, the following plugins are provided, each with an option to enable
	or disable them:
	* `autoclose`: automatically closes brackets, quotes, etc...
	* `comment`: provides automatic commenting for a number of languages
	* `ftoptions`: alters some default options depending on the filetype
	* `linter`: provides extensible linting for many languages
	* `literate`: provides advanced syntax highlighting for the Literate
	programming tool.
	* `status`: provides some extensions to the status line (integration with
	Git and more).
	* `diff`: integrates the `diffgutter` option with Git. If you are in a Git
	directory, the diff gutter will show changes with respect to the most
	recent Git commit rather than the diff since opening the file.
	Any option you set in the editor will be saved to the file
	~/.config/micro/settings.json so, in effect, your configuration file will be
	created for you. If you'd like to take your configuration with you to another
	machine, simply copy the settings.json to the other machine.

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:

micro/runtime/help/options.md

Lines 465 to 486 in dc77592

	Plugin options: all plugins come with a special option to enable or disable
	them. The option is a boolean with the same name as the plugin itself.
	By default, the following plugins are provided, each with an option to enable
	or disable them:
	* `autoclose`: automatically closes brackets, quotes, etc...
	* `comment`: provides automatic commenting for a number of languages
	* `ftoptions`: alters some default options depending on the filetype
	* `linter`: provides extensible linting for many languages
	* `literate`: provides advanced syntax highlighting for the Literate
	programming tool.
	* `status`: provides some extensions to the status line (integration with
	Git and more).
	* `diff`: integrates the `diffgutter` option with Git. If you are in a Git
	directory, the diff gutter will show changes with respect to the most
	recent Git commit rather than the diff since opening the file.
	Any option you set in the editor will be saved to the file
	~/.config/micro/settings.json so, in effect, your configuration file will be
	created for you. If you'd like to take your configuration with you to another
	machine, simply copy the settings.json to the other machine.

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 😛