I actually sent a patch yesterday, but thanks to your message I realised
that my messages weren't being sent (new mail provider, didn't configure
it properly).

I attached the patch below, and hope everything works now.

Dmitry Gutov <dgutov@yandex.ru> writes:

> Hey Philip,
>
> How's it going?

> On 21.07.2020 21:51, Philip K. wrote:
>> You're right, I forgot to stage that.
>
> I can fix up the minor nits and push the patch now, if you like.
>
> Just wanted to make sure you didn't come upon any more significant 
> problems in daily usage.


-- 
	Philip K.