Separate targets "make docs" and "make install-docs" for the documentation
It is no longer installed by default, but included in "make world"/"make install-world". Documentation updated accordingly. Also, fix vpathsearch function to work when calling make install-docs without previous make docs.
Showing
Please register or sign in to comment