Bug#814759: F1 is Help in GNOME Terminal

[Henrik Ahlgren]

F1 works in many terminals (e.g. plain xterm), but in GNOME it opens the
help window, unless the shortcut is disabled.

It would be useful if simple "1", "2", etc. would work instead of
function keys.