Lean Game server code editor mode

Stream: general

[Shreyas Srinivas]

I was playing with the set theory game (since it was just announced), and I had the following issue: I press the </> button to switch to the code editor mode. It stays that way until I go to the next challenge, which is again presented in typewriter mode.

[Shreyas Srinivas]

Could the setting be saved locally, instead of users having to change it every stage?

[Jon Eugster]

I usually collect ideas like this as github issues (https://github.com/leanprover-community/lean4game/issues) so they are collected in one place.

[Shreyas Srinivas]

Got it. Created an issue a few hours ago.