>>>>> "jg" == Juan Jose Garcia-Ripoll <juanjose.garciaripoll at googlemail.com> writes: jg> Eric, do you still have the same problem? I have tried on various Linux jg> boxes and never found this problem. Hi, No, the next time I updated from git the problem disappeared. Sorry for the false alarm. -- Eric Marsden