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 :)