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.