docgen linkifier

Stream: general

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/to_lin.html#matrix.to_lin'_submatrix

Why does this not linkify in the declaration below? image.png

I was hoping to tidy up this file doc-wise before the port to Lean4 and then I came across this.

[Eric Wieser]

The linkifier is different in lean 4 anyway, so I wouldn't worry about it

[Eric Rodriguez]

is it worth fixing the docs in this file before or after the port?

[Eric Rodriguez]

there's some issues (maps have been updated to be R^mop linear instead of just R-linear for example)

[Eric Wieser]

I think it's worth fixing the docs

[Eric Wieser]

But not worrying about things not linking

[Eric Wieser]

Since the markdown parser is not the same code in Lean4