7fea2bffc6
The fix commited in17f1bb50e4clashed withcc83ec0f74. The later is a more elegant solution that doesn't require to drop the header files from being installed. This commit reverts changes from17f1bb50e4.