(This will allow us to hack-fix wxWidgets' bug for determining the height when fonts are scaled. This commit includes such a fix, but I have no idea if this particular one will work or not.)
