On Sat, 15 Jun 2019, Ludovic Courtès wrote:
This is fixed (surprisingly easily!) by commit f3d797005374e5333c7596fe86b4a524ab1b9b11.
Neat!
Let me know if you notice anything wrong!
Everything looks good and works well for me.
Thanks for the bug report,
Thanks for the quick fix. Best, Jack
