Thanks. The reason I asked for a merge too is that I don't have permission to do so myself, and we don't have an automerge bot yet. Quoting Bill Burke (2018-05-17 12:45:39) > Approved. I didn't merge though.