Don't copy headers when not building docs.

[jtv]

In order to help Doxygen find all the headers, I had the docs target
copy all of them into the build tree (if that differed from the source
tree).

But it turns out that that was happening even on non-documentation
builds. Which makes development a little hard, because you're always
working with copies of the headers, stuck in the build tree!

For now, just skip the copying when not configured to generate
documentation. Later we can look into copying the headers somewhere
into the docs directory instead, so they don't get into the way of
the source build itself.