Red symbol highlights on github

Created by: muratsu

Currently, we highlight the symbol at the point with a yellow-ish color and other references to that symbol in red. The expected color is gray. Turns out, enabling the latest preview feature (dark high contrast) messes up our css colors.

Only Github is affected. It's happening on all browsers.