HOTKEY_VK_CODE   3255 src/w32fns.c   		      HOTKEY_MODIFIERS (key), HOTKEY_VK_CODE (key));
HOTKEY_VK_CODE   8812 src/w32fns.c     vk_code = HOTKEY_VK_CODE (hotkeyid);