updated for version 7.0074
diff --git a/src/gui_w48.c b/src/gui_w48.c
index 2e09655..48a87d9 100644
--- a/src/gui_w48.c
+++ b/src/gui_w48.c
@@ -1667,7 +1667,7 @@
* mapped we want to use the mapping instead. */
if (vk == VK_F10
&& gui.menu_is_active
- && check_map(k10, State, FALSE) == NULL)
+ && check_map(k10, State, FALSE, TRUE) == NULL)
break;
#endif
if (GetKeyState(VK_SHIFT) & 0x8000)
@@ -1781,7 +1781,7 @@
/* Check for <F10>: Default effect is to select the menu. When <F10> is
* mapped we need to stop it here to avoid strange effects (e.g., for the
* key-up event) */
- if (vk != VK_F10 || check_map(k10, State, FALSE) == NULL)
+ if (vk != VK_F10 || check_map(k10, State, FALSE, TRUE) == NULL)
#endif
DispatchMessage(&msg);
}