Message9577
Looks like we have identified the problem then, and it's the same one as this open issue with JLine2 - https://github.com/jline/jline2/issues/156 - also AltGr. But AltGr does not appear on US keyboards, so that's probably why we are seeing it as an issue - the usual internationalization problems!
Good intro to the topic in http://en.wikipedia.org/wiki/AltGr_key
We most likely will have to fix JLine2 to fix this problem. |
|
Date |
User |
Action |
Args |
2015-03-03 23:12:33 | zyasoft | set | messageid: <1425424353.75.0.80653193334.issue2275@psf.upfronthosting.co.za> |
2015-03-03 23:12:33 | zyasoft | set | recipients:
+ zyasoft, pekka.klarck |
2015-03-03 23:12:33 | zyasoft | link | issue2275 messages |
2015-03-03 23:12:33 | zyasoft | create | |
|