felix . winkelmann Wed, 16 Sep 2020 10:21:48 -0700
> Hi all, > > Here's a fix for #1703. The commit message says it all. >
Pushed, thanks. felix