We found the reason for the behavior. To create shorcuts for menus, the EiffelVision2 syntax is to use an ampersand before the letter where the shortcut will be, e.g. &File.

However on GTK, the character used for this purpose in the underscore, not the ampersand. As a result, we do an escape of the _ to be __ so that they appear as _ in the menu, but we only do the escape if there is an ampersand. All the menu entries you mentionned do not have an ampersand and the escape is not done.

We are changing the mechanism so that we do the escape whenever there is a _ or a & in the string.