Vertically resizable text areas

[nicknytko]

It would be nice if the text area element could either be vertically resizable, or if it automatically fills the page. This could probably be done by a css property:

https://developer.mozilla.org/en-US/docs/Web/CSS/resize

My use case:

it would be nice to have more room to edit text.

[inducer]

Totally agree. #1012 contains a switch to CodeMirror 6, which makes the editor as big as the text contained in it, instead of having it be independently scrollable. That should address the concern, I think (in addition to avoiding burning people's retinas at night).