Fix bug #3389 ‘document 'F12' shortcut’