Hi Marc, > thanks for catching that. The proposed change is perfect.
OK, pushed it. > Actually, I > had made that fix in my local code as well so I am wondering why it > didn't make itself into the patch I sent you. What I committed in your name on 2020-06-25 was what you had sent to the list on 2020-05-20. If you do "git status" regularly, you will notice pending patches of yours. Bruno
