open_locale is red

Stream: general

[Patrick Massot]

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.

[Gabriel Ebner]

Please file an issue.

[Patrick Massot]

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

[Patrick Massot]

I was opening it.