This change is not meant to change any functionality, only move some
Bash-specific logic out of the `Makefile` into its own script:
`install-include-headers.sh`. This reduces the perceived complexity of
the `Makefile` but the complexity is still there, tucked away in this
script. This script also has the advantage that it can be run separately
if needed.
This commit comes after a few different attempts at building up
`Makefile` lists of headers to copy over along with the various
locations they must be copied from. It is certainly possible to do this,
but due to how we need to remove some headers from the list, it ends up
being easier to just `cp` and then `rm`, which this script retains.
