Closed tpadioleau closed 4 years ago
Fixes #75.
Thank you very much. I've cherry-picked your commit to the master, so now you can safely remove your branch.
Relevant commit is b5c6f09d79c3e807a831a5fc0005e44ae8a97c55
Fixes #75.