+ * FREEGLUT_MENU_FONT can be any freeglut bitmapped font.
+ * (Stroked fonts would not be out of the question, but we'd need to alter
+ * code, since GLUT (hence freeglut) does not quite unify stroked and
+ * bitmapped font handling.)
+ * Old UNIX/X11 GLUT (BSD, UNIX, IRIX, LINUX, HPUX, ...) used a system
+ * font best approximated by an 18-pixel HELVETICA, I think. MS-WINDOWS
+ * GLUT used something closest to the 8x13 fixed-width font. (Old
+ * GLUT apparently uses host-system menus rather than building its own.
+ * freeglut is building its own menus from scratch.)
+ *
+ * FREEGLUT_MENU_HEIGHT gives the height of ONE menu box. This should be
+ * the distances between two adjacent menu entries. It should scale
+ * automatically with the font choice, so you needn't alter it---unless you
+ * use a stroked font.
+ *
+ * FREEGLUT_MENU_BORDER says how many pixels to allow around the edge of a
+ * menu. (It also seems to be the same as the number of pixels used as
+ * a border around *items* to separate them from neighbors. John says
+ * that that wasn't the original intent...if not, perhaps we need another
+ * symbolic constant, FREEGLUT_MENU_ITEM_BORDER, or such.)