This is mostly cosmetic, but it might fix build failures, on some
platform, when copying from the documentation.

Back-patch to 9.3 (all supported versions).