Commit 5d74565a961e790ba7f28e8e44a81fb45127fd21
2018-04-19T09:39:39
Give priority to the build directory headers Not changing anything right now AFAIK. But if for any reason in the future we end up with two headers with the same name in the source and build directories, chances are we want to use the one in the build directory.