On 13 Oct 2024, at 19:48, Marco Antoniotti <marco.antoniotti@unimib.it> wrote:Hello parenthetical crowdIs there a consensus about how to "name" Unicode characters, or every implementation does whatever it likes (thus breaking otherwise perfectly portable code)?Cf., #\INFINITYAll the bestMAPS Do not even think to use the "hey, it is an implementation-dependent thing" argument!--Marco Antoniotti, Professor tel. +39 - 02 64 48 79 01
DISCo, University of Milan-Bicocca U14 2043 http://dcb.disco.unimib.it
Viale Sarca 336
I-20126 Milan (MI) ITALY