Switch from the shortcut.js to the jquery.hotkeys.js library.

The original shortcut.js library has trouble handling special keys.
For example, is a shortcut for 't' is defined, pressing F5 will
trigger it because the keycode for F5 is equal to the charcode for
't' (116).