Am 13.05.2025 um 13:14 schrieb Theodoros Panagiotidis:
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