Merge pull request #14044 from duglin/MakeDocs

Add back top-level "make docs"