Created attachment 147390 [details] add OPTIONS_DEFINE=DOCS to Makefile Make installation of DOCS optional by adding a DOCS option.
Submitter is committer
Was already resolved.