PSA uncolor backticks

Stream: general

[Martin Dvořák]

I found a way how to color-highlight the stuff inside backticks but not the backticks themselves in VS Code!
It significantly improves readability of stuff like M' in the comments.
https://github.com/madvorak/vscode-lean4-colors/blob/9f3e7b9221ca73f62fcb34febe3209e8791d5aa3/settings.json#L143