Re: terminal @number vs. @user-number

[Akim Demaille]

Le 22 oct. 07 à 02:18, Joel E. Denny a écrit :

What do you think?

I, too, have needed, at occasion, to know the genuine number
of the symbols.  The XML output should certainly contain too
much information rather than not enough.