>>>>> "Enrico" == Enrico Forestieri <[EMAIL PROTECTED]> writes:
Enrico> On Tue, Oct 31, 2006 at 09:01:53PM +0000, José Matos wrote: >> On Tuesday 31 October 2006 8:03 pm, Enrico Forestieri wrote: > I >> simply want to be sure that nobody has a better solution and avoid >> > a commit/revert ping pong. >> >> If Jean-Marc and Georg agree that is fine with me. :-) Enrico> I have just commited it, José. Georg already agreed and I Enrico> don't think JMarc has big objections. As I said, this patch Enrico> does not preclude doing things more correctly by taking into Enrico> account the catcode associated to a char. Doing so would take Enrico> much longer, though. Your patch is OK. JMarc
