>>>>> "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