On Sat, Sep 19, 2020 at 11:56:07PM +0200, Thibaut Cuvelier wrote: > I just pushed a new version without that operator (and many more comments, > by the way). Is that better for you? It works now, thanks. Pavel