Small gcdext_1

[Marco Bodrato]

Ciao,

Il Dom, 24 Novembre 2019 8:41 pm, Torbjörn Granlund ha scritto:
> nisse at lysator.liu.se (Niels Möller) writes:
>   BTW, looking at recent changes to that file, a ± character (plus/minus,
>   unicode 0xb1, TeX \pm) was deleted in 46b4c2e7f148. Is it important to
>   avoid non-ascii, and if so, what's the preferred way to write this
>   symbol? "+/-" ?
>
> Ask the perpetrator.  :-)

Uhm, I removed it because I got a warning on some platform... but I do not
even remember which one... On the terminal I was using, it was printed as
a question mark "?", I did not notice it was an intentional plus/minus "±"
character!

You can write it as "+/-", as you like. Or you can also reinsert the
unicode character, I'll try to remember to ignore any warning I may see
about it.

Ĝis,
m