Skip to content

Conversation

jserv
Copy link
Contributor

@jserv jserv commented Feb 15, 2025

This adds a catch to an exception that might occur when leaving a menu which is not shown by the parent menu. This might occur, for instance, when searching for the symbol of a named choice.

This adds a catch to an exception that might occur when leaving a menu
which is not shown by the parent menu. This might occur, for instance,
when searching for the symbol of a named choice.

Signed-off-by: Jim Huang <jserv@ccns.ncku.edu.tw>
@jserv jserv merged commit 915e7bc into main Feb 15, 2025
3 checks passed
@jserv jserv deleted the fix_leaving_menu branch February 15, 2025 15:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants