>>>>> "José" == José Matos <[EMAIL PROTECTED]> writes:

José> On Monday 09 July 2007 18:12:48 Bo Peng wrote:
>> Jose, if you can not decide, just toss a coin. IMO, both approaches
>> are good enough. :-)

José>   OK then, let us go Jean-Marc's way, and proceed for other more
José> pressing issues.

I committed a slightly updated patch.

JMarc

Reply via email to