-
Notifications
You must be signed in to change notification settings - Fork 29.4k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add settings for changing the workbench font size and font #144365
Add settings for changing the workbench font size and font #144365
Conversation
This PR adds the settings necessary for setting a font size and font family for the workbench and applies it in themeing.ts. I'm not sure if anything else is necessary like watching for changes to the settings and applies them retroactively. |
691cac3
to
904a1ee
Compare
@sbatten, any word? |
c926479
to
904a1ee
Compare
9607f58
to
904a1ee
Compare
Same discussion starting from #63602 (comment) applies here again. |
Ah, okay, I see the issue. I will attempt to find as many instances as I can of certain pixel values being hardcoded and alter them. |
I think I got all of the hardcoded values, but I'm not entirely sure. |
4c73c99
to
5c96bea
Compare
Tests should be green now. |
The PR is very large. I wonder if maintainers are more likely to accept it if we split the PR:
If the first PR is merged and the 2nd PR is small enough, my team at Google can help test it and iterate on it. |
@laurentlb I'm happy to split this PR. How would you like to open up communication for that? |
I'm going to close this for now while @laurentlb and I work towards splitting this PR up and getting changes made through at a much slower and more deliberate pace. |
@ElijahPepe @laurentlb thanks for doing that. Please ping me on any new PRs you open. |
This PR fixes #519.
This does need to be refined a bit; I did this rather hastily.