On 12/12/2009 15:53, Mike Massonnet wrote: > I want to come back on what I said about Terminal, it has only an > option to disable F10, but not Shift+F10. That beeing said, Shift+F10 doesn't do anything at all in Terminal here. -- Yves-Alexis