On 1 May 2018 at 22:56, François Dumont <frs.dumont@gmail.com> wrote: > Hi > > If not told otherwise I'll commit attached patch tomorrow. Commit it where? The 8.1 release is not out yet, so we shouldn't be pushing new stuff onto trunk yet. Nor should we push such stuff into the release branch.