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

From: Lars Ingebrigtsen <[email-masked]>
Date: Tue, 01 Oct 2019 18:32:24 +0200

Eli Zaretskii <[email-masked]> writes:

> I actually am not sure a click on the margins should produce the same
> effect as on the text area.  The margins are used to display different
> text from what's in the text area, so I'm not sure I understand the
> rationale.

Oh, I assumed that this was about scrolling, but that's probably not
what <double-wheel-down> does?

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no