69c3b39d0d
Because 'doc' is a directory, when running `make doc`, you'll see this: make: Nothing to be done for `doc'. By adding a target for `doc` to build `docs`, both work. Fixes #14705