This was more trouble than it is worth:
- remove_directory fails if doc/ is not owned by the user
- some devs build in-tree, then deleting doc/ breaks the build
- `make install` isn't affected by the stale files at all: the tags are
built before install-time
So, reverting this change means only that devs who use a build/
directory will need to delete build/runtime/doc/ on the occasion that we
rename a doc file.
If a help file is renamed, stale help files in the build workspace will
cause duplicate tags (which causes the build to fail). To avoid this,
always delete build/runtime/doc/ before building helptags.
Specify that the ${GENERATED_HELP_TAGS} "command" (output) depends on
`helptags` so that it always regenerates the doc/ tags. (cmake "targets"
always run, whereas "commands" are contingent on their dependencies. But
we don't define doc/ dependencies because they are circular.)
Declare dependency in terms of directory, rather than individual doc
files to avoid target dependency cycles. This still maintains install
targets at doc file level.
I see that problem fixed by #2801 was resurrected by making help tags file
generated in a more direct way. This fixes the hang without using the empty
file.
