On Thu, Sep 20, 2018 at 08:23:45AM +0200, Adrien Nayrat wrote:> Yes, here is the patch.
Thanks Adrien. I have reworded a bit the thing, fixed a typo, andpushed down to v11 where this applied without conflicts.--Michael