bug#5557: <left-margin> <double-wheel-down> is undefined

[martin rudalics]

> That's true.  Hm...  perhaps the user has really big margins?  That
> would make the issue more apparent there -- and it's difficult to say
> what else the scroll wheel should do there other than work the same as
> in the main portion of the buffer.

Nowadays practically all applications scroll the window vertically
regardless of where the mouse pointer is - even when it's on the
horizontal scroll bar.  The only exception is the title bar where some
window managers optionally "roll" the window in or out.

martin