Merge pull request #13271 from seamuslee001/header_whitespace_fixes
authorMonish Deb <monish.deb@jmaconsulting.biz>
Thu, 13 Dec 2018 14:31:22 +0000 (20:01 +0530)
committerGitHub <noreply@github.com>
Thu, 13 Dec 2018 14:31:22 +0000 (20:01 +0530)
(NFC) whitespace header fixes


Trivial merge