Ricardo Wurmus Wed, 13 May 2020 14:54:42 -0700
I believe this was fixed by commit 21fcfe1ee969cc477dc41486ae4074e655d44274.
Closing. -- Ricardo