Please push #173 and #176 into main

Hi Pierre-Antoine,

I understood that during the last call we approved pull requests #176 and #173. I also promised to propose some changes until Wednesday. It would make my work easier if you could merge the approved PRs into the draft. Currently I’m working from the editors draft but I’m quite confident that that is a messy way to operate.

Best,
Thomas

Received on Monday, 7 June 2021 12:08:29 UTC