plugins: Run deinit() on exit() of micro

[JoeKar]

This came up with #4230 and allows plugins to do some finalization stuff.

[dmaluka]

The idea seems reasonable. Although I'm a bit concerned that there might be some plugins that are using deinit() for doing some stuff which they are not expecting to be done on exit...

Trying to find out what was the original use case for this deinit() callback... This callback was introduced in commit 4027081 to support the built-in linter plugin (added in the same commit), as if the linter plugin used deinit() (it didn't, and it still doesn't). Splendid.

Possibly deinit() has never been actually used by anyone, ever. https://github.com/micro-editor/micro/issues?q=deinit doesn't give any insight about any actual users either.

[achadwick]

If current behaviour needs to be maintained, then a new at-exit cleanup hook plus documentation of exactly what fires when would seem appropriate.

But, if there are really no plugins out there that have one, go for it. It isn't unreasonable for plugins to receive deinit() as the editor exits, especially if they already init() at startup.

[dmaluka]

But, if there are really no plugins out there that have one, go for it. It isn't unreasonable for plugins to receive deinit() as the editor exits, especially if they already init() at startup.

Yeah, I agree with that.