Web editor reload on window resize

Stream: general

[Eric Paul]

When using the web editor, https://live.lean-lang.org/, if the window is resized sufficiently it says "Waiting for Lean server to start" and restarts the file after some wait. This is a bit inconvenient for me as I'm often resizing my window. Just wondering if this is intended behavior or if it could be fixed.

[Jon Eugster]

I would guess this is if it goes from desktop layout (infoview to the right) to mobile layout (infoview below), isn't it? the threshhold is 800 pixels if I remember correctly.

If it annoys you, you can go to the editor's setttings, choose the preferred layout and select the option to save your preferences in a cookie. That way it shouldn't happen.

Out of curiosity what's your workflow which requires constant resizing of windows?

[Eric Paul]

Yes, it's precisely that. Awesome, fixing it at the mobile layout seems to work, thanks!
(I still wonder if it's possible to let it move the infoview around without restarting everything)

I program on a laptop and so like to have the window I'm programming in be fullscreen. I then keep another window that I want to be referencing behind it taking up the right half of the screen. I'll make the window I'm programming in take up the left half of the screen whenever I want to reference the window behind it. Hopefully that makes sense