> Merge early is pretty much my default position ... and that applies to this > context in my view.
Thank you Tim for your quick and clear consent. Meanwhile, pull request #9333 and its counterpart #9681 for the 1.1.1 stable branch have been approved by Richard. Unless I hear any protest until Sunday afternoon (CEST), I would like to merge in the evening, just in time before the Australian plumbers start their weekly shift again. Matthias