On Mon, Oct 23, 2023 at 08:49:53PM +0000, Alan Mackenzie wrote:
> Hello, Eli.

[...]

> I have always disliked the replacement of ASCII characters by non-ASCII
> Unicode punctuation in working documents [...]

Not a devel here, by a long stretch, so count me as anecdotal, but I'm
with Alan here.

Cheers
-- 
t