Editor font size

[rooton]

Font is too big. Please add font size change ability to setting.

P.S

if you don't plan to do it, just write. Please don't give such stupid answer like https://github.com/JetBrains/kotlin-playground/issues/45

[AlexanderPrendota]

@rooton Hello! Thank you for the feedback.

You can add some css-styles to your playground component. What kind of settings do you want to?

1. Add another attribute in attributes ?
2. Add another option in options ?

Thanks.