- changed the Shift+XX menubar shortcuts into either Ctrl+XX or
  Ctrl+Shift+XX (we shouldn't use Shift+XX shortcuts in the menubar,
  in particular on Mac, where the shortcuts conflict with input
  text fields)

- exchanged the meaning of Ctrl+s and Ctrl+Shift+s, as this is what
  most people expect