Disable hovers on docstring headers?

[david-christiansen]

When documentation from Lean is rendered inline in a manual, the header of the documentation shows the thing being documented (function, tactic, inductive type, etc) with full semantic highlighting. This can create a silly effect, because readers get a popup hover with exactly the same information that's below/next to it!

Perhaps hovers on docstring headers should be disabled when their contents would be redundant with the text immediately next to them on the page.