>
> We could do that, yes.  The downside is that this requires special 
> handling in src/keyboard.c, which is ... delicate ;-)
>

I don't think it is really useful to add such a special handling to fix 
this bug (but it could make sense to add it later).  I attach the updated 
patch, which I think does the right thing.