[[ Bug 14155 ]] Fix to the Menu Builder

This replaces the branch bugfix-11573, since a specific bug report has been opened for the IDE issue.
There is still a fix to bring to the documentation (see the bug 11573).