Graceful fallback if pandoc is unavailable

Closes #4801

diff --git a/docs/Makefile.am b/docs/Makefile.am
index 24d4e150e53783cc1642a6d2a9c781b871738c0f..5d71594c52a46a83a7ef77e20ccf37586b865d03 100644 (file)
--- a/docs/Makefile.am
+++ b/docs/Makefile.am
@@ -53,8 +53,7 @@ clean:
 else
 if !HAVE_MANPAGES
 $(MANPAGES_TARGET_ALL):
-       echo "You need pandoc to generate the manpages"
-       exit 1
+       @echo "Pandoc is required to build $@"
 endif
 endif