On Mon, Oct 11 2021, martin rudalics wrote:

> Or maybe I was just waiting for Peter

Sorry. I was waiting for the push to master before using it...

(But I've tested it once, and it worked.)

-- 
           Peter