Zulip Chat Archive

Stream: general

Topic: open_locale is red


view this post on Zulip Patrick Massot (Jul 07 2020 at 14:30):

We can now use open_locale right after the imports, but it seems the Lean server info request doesn't know about that:
open_locale.gif
Note that I don't think the new widgets have anything to do with this issue. Of course it has pretty low priority, but this little bug could still puzzle beginners.

view this post on Zulip Gabriel Ebner (Jul 07 2020 at 14:31):

Please file an issue.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:32):

https://github.com/leanprover-community/lean/issues/382

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:32):

I was opening it.


Last updated: May 08 2021 at 03:17 UTC