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

From: Lars Ingebrigtsen <[email-masked]>
Date: Thu, 13 Aug 2020 10:42:12 +0200

Stefan Kangas <[email-masked]> writes:

> I have attached a patch which implements this functionality.
> Any comments?

I don't use a scroll wheel mouse, but it sounds like a good idea to me.

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