Hi, > > But I can cut & paste the paragraph above into the commit message and > > resend. Or should I redo the github pull-request instead? > > I can amend this information. Great. thanks, Gerd