MENU_HOT_COLOR     89 lib/skin/colors.c     { MENU_HOT_COLOR, "menu", "menuhot" },
MENU_HOT_COLOR    162 lib/widget/menu.c             tty_setcolor (color == MENU_SELECTED_COLOR ? MENU_HOTSEL_COLOR : MENU_HOT_COLOR);
MENU_HOT_COLOR    216 lib/widget/menu.c         tty_setcolor (hotkey ? MENU_HOT_COLOR : MENU_ENTRY_COLOR);