On Fri, 7 Nov 2008, Riccardo (Jack) Lucchetti wrote:
On Fri, 7 Nov 2008, Allin Cottrell wrote:
> There's no reference to mathtime in the current TeX manual
> sources...
Actually, mathtime is used in the Portuguese translation.
Well spotted. I've now removed that.
Allin.