You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It is actually much worse than that. We do a really terrible job parsing names to link to right now (though it's better than nothing of course). The place to look is here:
I tried to track this down a bit and by the time we get to the code you linked the text has already been split before the prime. Highlighting doesn't seem to be the culprit. If I skip the likify step in diagrams-doc the html result has the whole name in one node. So I'm not sure what is going on.
In the manual links to names that end in a prime are linked to haddocks as the unprimed name.
The text was updated successfully, but these errors were encountered: