|
| From: | Hans Aberg |
| Subject: | Re: terminal @number vs. @user-number |
| Date: | Sun, 28 Oct 2007 11:03:55 +0100 |
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
| [Prev in Thread] | Current Thread | [Next in Thread] |