Closed mitchellwrosen closed 5 years ago
This patch partially fixes #43, I think I'll close that out and re-open a new ticket. Main problem: if you hover over e.g. Foo in the term
Foo
blah : Foo -> Bar -> Foo
then both Foos will have their own tooltip T_T
This patch partially fixes #43, I think I'll close that out and re-open a new ticket. Main problem: if you hover over e.g.
Foo
in the termthen both
Foo
s will have their own tooltip T_T