On Tue, Sep 15, 2020 at 10:16 AM Robert Pluim <rpluim@gmail.com> wrote:

> >>>>> On Tue, 15 Sep 2020 00:04:05 +0200, Mathias Dahl <
> mathias.dahl@gmail.com> said:
>
> Nitpicking below. Nothing major, it looks to be a useful feature.
>

Hi Robert, thanks for this! I will review your suggestions and incorporate
the ones I like :)