Merge commit '70b42d0d' (whose cod is already included)

Commit 70b42d0d is currently proposed_master, so by our agreements with
GSI we can't remove it from history.  The change itself is already
in master (but with typos fixed in the commit message). So let's
pin the commit by merging, even if it will appear twice in the history.