On Tue, Mar 15, 2011 at 11:03 AM, Bo Jacoby <bojacoby at yahoo.dk> wrote: > 3 3 3?10 is two characters shorter than 3?10 10 10 and so it should be preferred. And 3?3#10 is shorter than both, though is closer to 3?10 10 10 than 3 3 3?10. -- Raul