Gnome Terminal captures F10 instead of passing it to the shell. I want to disable it. Searching for the problem returned answers that it can be disabled in "Preferences/Shortcuts". However, it doesn't appear to be there for me.
I have Ubuntu 16.04 and Gnome Terminal 3.18.3.
