[sr-dev] git:master:dd36b50f: Makefile: do not install old unmaintained doc-related files