[BLUEJ-903] AltGr+digit inadvertently triggers the Ctrl+digit tab selection shortcut
In the editor window, we let Ctrl+8 select the 8th tab. However, AltGr+8 is used on some German keyboards to enter special characters. Because Java maps AltGr->Ctrl+Alt, the AltGr+8 becomes Ctrl+Alt+8, which inadvertently triggers the Ctrl+8 shortcut. We should distinguish between AltGr and Ctrl, probably by checking if Alt is also pressed.
Issue metadata
- Issue type: Bug
- Priority: Medium
- Fix versions: 4.0.1