References in docs

Stream: general

[Ruben Van de Velde]

Are the references like here https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html to MR32592 supposed to be links?

[Johan Commelin]

Yes, I think they should be...

[Bryan Gin-ge Chen]

it’s a missing feature at the moment: doc-gen#61