3.5.7 - customize shortcuts

Feature changes:

• #141: allow customized shortcuts
• #495: add new shortcuts: translate page, edit page, copy page text, add bookmark, delete term

Tweaks:

• #497: Change default port to 5001.
• #500: show popup for ignored terms with data
• Add version to startup console.