Is there a way to change the font size of everything in the UI (all 10 elements under preferences -> colors & fonts -> fonts) all at once -- the way the increase/decrease font size buttons work in Word or something equivalent?
The immediate reason is that Windows 10 keeps playing with font sizes as I adjust the UI scaling and screen resolution, and sometimes for other reasons (like after a Dell system health scan which exercised the display in a lot of weird ways). DO responds in sometimes unexpected ways. But even when it does the expected thing, it's a nuisance to keep having to adjust all 10 fonts individually.