Zulip Chat Archive

Stream: general

Topic: doc request


view this post on Zulip Scott Morrison (May 30 2020 at 04:01):

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/)

view this post on Zulip Scott Morrison (May 30 2020 at 04:01):

I'm actually not certain how to do this.

view this post on Zulip Scott Morrison (May 30 2020 at 04:02):

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

view this post on Zulip Scott Morrison (May 30 2020 at 04:05):

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"

view this post on Zulip Mario Carneiro (May 30 2020 at 04:08):

the google search bar works for me

view this post on Zulip Mario Carneiro (May 30 2020 at 04:09):

what browser are you using? I am on FF

view this post on Zulip Scott Morrison (May 30 2020 at 04:11):

chrome

view this post on Zulip Scott Morrison (May 30 2020 at 04:11):

It's come good for me now.

view this post on Zulip Scott Morrison (May 30 2020 at 04:11):

transient issue, I guess


Last updated: May 14 2021 at 06:16 UTC