Ludovic Courtès Sun, 11 Nov 2018 09:31:12 -0800
Closing this bug, which Efraim addressed in commit b44b1f08f6945ea8370746cfdadb44c7dea9ea3e.
Thanks! Ludo’.