live lean save editor settings not working on Firefox

Stream: general

[Shreyas Srinivas]

As the title says the save settings feature doesn’t seem to work on Firefox. In particular I would really like to save the checkbox to accept suggestions when the enter key is pressed. This is becoming a painful footgun for me every time I open the editor.

[Jon Eugster]

Reproduced, I'll try to take a look. lean4web#71