On 8/26/2020 1:28 PM, Jonas Gunz wrote:
Would you generally be interested in merging such a change?

I like it, and I'm using it! https://cogarr.net/source
Even if it doesn't get merged into the main repository, it might be
helpful to have a list of "useful or popular patches" somewhere.