In reviewing an off-the-shelf Web-browser-based application, I found the
following font setting in several places among the default CSS files:
font: menu;
I can't imagine the designers thought that anyone would have a font
called "menu" on their computers, and "menu" isn't one of the standard
font-family values like serif or monotype. Is this somewhere else in the
standard, or do any of you know a platform that defines an extension
like this?