Re: terminal @number vs. @user-number

[Hans Aberg]

On 28 Oct 2007, at 02:24, Joel E. Denny wrote:

What about @symbol-number and @token-number?

I think those are fine:

It seems everyone is in agreement, ...

Yes.

...so I committed the following.

Fine.

  Hans Aberg