Merge branch 'master' into 3.2

Note: This merge is a no-op, it adds #4074 but removes all its changes,
as we don't want to remove content from 3.2 docs.
This merge enables us to further use `git merge master` to get `master`
changes into `3.2` without worrying about those removals, as they have
been handled in this commit.