On 2020-01-09 16:16, Mark Johnston wrote: > Sorry, I committed a different patch in r356555 before seeing this. I thought of your version first too. You can decide, I think my version is more clean. --HPS