Thanks for this!

Please find attached the revised script.

Hope this is useful to all.

Thanks, Theo.

Just two trivial syntax remarks which perhaps are also mildly interesting for others:

- one can write "set verbose off" to cover both "set echo off" and "set messages off" at the beginning (this was introduced at least five years ago)

- also for some years it has been the default to have quiet loops, so writing "loop ... --quiet" isn't necessary anymore (since 2020c)

cheers

sven