Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Add separate editor font size option #1027
Based off my own use and this thread on the discourse I thought it would useful to set the editor font size separate of the style.zoom. In my own use case all the graphic elements are a decent size, but the editor font is a touch small.