Zulip Chat Archive

Stream: mathlib4

Topic: docs4 broken

Johan Commelin (Jan 14 2023 at 04:26):

I think docs are broken, see docs4#List

Eric Wieser (Jan 14 2023 at 08:26):

In that the docstrings are being rendered as monospace?

Johan Commelin (Jan 14 2023 at 13:18):

I get Cannot fetch data, please check your network connection. Error: fail to open indexedDB declaration-data of version 1

Henrik Böving (Jan 14 2023 at 13:39):

For me that loads without issues.

Henrik Böving (Jan 14 2023 at 13:39):

image.png

Last updated: Dec 20 2023 at 11:08 UTC