I would like to change the font settings for developer-tools, like default font family and sizes (and generally have a more refined control of how textual information is displayed). I have found some information scattered around on how to do this (such as this Stack Overflow thread) but it seems like creating a userChrome.css style sheet is a legacy, semi-deprecated way of customizing the developer-tools UI. Is there a better way of accessing and customizing these settings?
