HOTKEY_MODIFIERS 3222 src/w32fns.c   		      HOTKEY_MODIFIERS (key), HOTKEY_VK_CODE (key));
HOTKEY_MODIFIERS 8780 src/w32fns.c     w32_modifiers = HOTKEY_MODIFIERS (hotkeyid);