On Thu, May 25, 2017 at 09:22:17PM +0200, Rainer Jung wrote: > > Should I open a GH issue or pull request for that trivial change? Yes. Everything is required to be reviewed, and we use github for that. Kurt