[PATCH 19/12] docs: Fix install-man$(1)-pages if no manpages are generated

[Andrew Cooper <andrew.cooper3@xxxxxxxxxx>]

All tools to build manpages are optional, and if none of them happen to be
present, the intermediate working directory may not even be created.

Treat this as non-fatal, bringing the behaviour in line with install-html.
Like the html side, it needs to be not-or to avoid Make thinking the rule has
failed.

Signed-off-by: Andrew Cooper <andrew.cooper3@xxxxxxxxxx>
---
CC: Anthony PERARD <anthony.perard@xxxxxxxxxx>
CC: Juergen Gross <jgross@xxxxxxxx>
CC: Roger Pau Monné <roger.pau@xxxxxxxxxx>
CC: Jan Beulich <JBeulich@xxxxxxxx>
CC: Stefano Stabellini <sstabellini@xxxxxxxxxx>
CC: Julien Grall <julien@xxxxxxx>
CC: Oleksii Kurochko <oleksii.kurochko@xxxxxxxxx>
---
 docs/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/Makefile b/docs/Makefile
index 966a104490ac..b30cc619f8dd 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -151,7 +151,7 @@ man$(1)-pages: $$(DOC_MAN$(1))
 .PHONY: install-man$(1)-pages
 install-man$(1)-pages: man$(1)-pages
        $(INSTALL_DIR) $(DESTDIR)$(mandir)
-       cp -r man$(1) $(DESTDIR)$(mandir)
+       [ ! -d man$(1) ] || cp -r man$(1) $(DESTDIR)$(mandir)
 
 # Clean
 .PHONY: clean-man$(1)-pages
-- 
2.39.2