Merge #11901: post-commit review fixes per Georg Brandl