On 2020-07-05 11:14, Paul Eggert wrote: > On 7/2/20 2:37 PM, Bernhard Voelker wrote: >> The attached fixes it. >> Okay to push? > > Thanks, looks good.
Thanks, pushed. Have a nice day, Berny
On 2020-07-05 11:14, Paul Eggert wrote: > On 7/2/20 2:37 PM, Bernhard Voelker wrote: >> The attached fixes it. >> Okay to push? > > Thanks, looks good.
Thanks, pushed. Have a nice day, Berny