Hello,

Sorry for answering late.

On Mon, May 20 2019, Tomi Ollila wrote:

> It is wiki -- look around the web page to see how to update.

Thanks, I didn’t know it was wiki.  I’ve pushed the amendment.

[...]

> s/patch/commit/ -- it is no longer patch when applied!
> 
> it may be possible that db could amend this...

You’re right.  I’ve amended the commit message.

-- 
Leo Vivier