Am 30.12.2022 um 20:04 schrieb Javier Sansa:
Thank you for the report, Javier - and also for the wishes. One more
time today I'll say sorry for the delay, there apparently has been a
technical problem with the mailing lists.
I can easily replicate your problem, this bug must somehow have crept in
recently, because I'm fairly confident this thing worked when all these
options were first introduced (about a year ago?).
This problem should now be fixed in git and snapshots. I too would like to thank Javier
for a very clear error report.
Allin Cottrell