Fix double hovers

Created by: beyang

GitHub now has jump-to-definition (https://help.github.com/en/articles/navigating-code-on-github). This uses a different approach than our code intelligence (mostly less accurate AFAICT), but the fact that now 2 sets of hovers appear (and jump-to-def behavior is unclear) affects usability of the Sourcegraph browser extension. I can't screenshot it because it looks like the GitHub feature is down right now, but we should proactively address the usability issues for our users. Screenshot:

Initial proposal: add a settings toggle that lets people toggle Sourcegraph vs. GitHub hovers depending on what they'd like to see.

@lguychard and @felixfbecker can you own prioritizing this ASAP?