doc request

Stream: general

[Scott Morrison]

Could https://leanprover-community.github.io/contribute/doc.html please contain instructions for adding hyperlinks to other files? (e.g. to link from a file under src/ to a file under archive/)

[Scott Morrison]

I'm actually not certain how to do this.

[Scott Morrison]

I guess another request: pages like https://leanprover-community.github.io/theories/sets.html should include links into the source code.

[Scott Morrison]

Also (I'm new to trying to use the online docs, and apparently having trouble :-) it seems the google search box on the online docs is broken?

e.g. if I go to https://leanprover-community.github.io/mathlib_docs/linear_algebra/sesquilinear_form.html, and in what I think is meant to be a search box on the top right (it says "enhanced by google") I type "category" and click the magnifying glass, I get the very unhelpful "Unauthorized access to internal API. Please refer to https://support.google.com/customsearch/answer/4542055"

[Mario Carneiro]

the google search bar works for me

[Mario Carneiro]

what browser are you using? I am on FF

[Scott Morrison]

chrome

[Scott Morrison]

It's come good for me now.

[Scott Morrison]

transient issue, I guess