Ctrl-click on `Substring.Raw.prev`

Stream: lean4

[Damiano Testa]

In the code below, Ctrl-click on Substring.Raw.prev takes to the correct file on line 91. However, docs#Substring.Raw.prev is on line 107, with doc-string starting on line 100.

#check Substring.Raw.prev

[Damiano Testa]

I tried it again and now it goes to the correct line!

[Damiano Testa]

Here is a picture showing what I sometimes see:

image.png

[Marc Huisinga]

Thanks for the report! lean4#12000

[Kim Morrison]

Note that we had to revert lean#12000, and lean#12150 now tracks this still open issue.