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