Feature request: Editor font size about openjscad.org

[Spiritdude]

I don't have access to high DPI display, so - do you have a copy of OpenJSCAD running locally? Add following lines into index.html near line 46:

.ace_scroller {
font-size: 10pt;
}

and let me know if the font is readable now.

[Spiritdude]

I added .ace-chrome {} declaration to define 10pt font - I may later add more settings for the editor.

[morsch]

Don't have a high-DPI device available, either, I just assumed (hence my writing "it must be..."). I think it's very small on a 24in display, though, and I know a lot of people who are used to larger fonts than I use.

I think 10pt is slightly bigger than 12px on regular, so it's a start.