Fix headers that were broken by #1510#1522

Merged

williamfgc merged 1 commit intoornladios:masterfrom KyleFromKitware:fix-broken-headers

Jun 19, 2019

+59-59

Commits on Jun 19, 2019

Fix headers that were broken by ornladios#1510
KyleFromKitware
committed