@stefanseefeld Since time will run short soon, I have to nudge you to ensure you got this on time. Please, have a look at
Thanks @lpranam for heads up!
develop, no ? Is there anything left to do ? (other than merge
master, I mean ?)
developis complete, i.e. there are no other expected commits targeted for 1.72.