Jocelyn, Thomas,
Jocelyn, your patch works perfectly - thank you. May I leave it to the two of you to decide what should happen about propagating this patch ? (I have set out my user's point of view about it in my email of Fri, 28 Jul 2023 10:11:00 +0100, but obviously my opinion is not binding on either of you.) I would be glad to hear what you eventually decide between you. Many thanks indeed for your help ! Roger.
