1 files changed, 6 insertions, 0 deletions
diff --git a/dist/s_docs b/dist/s_docs
index 7b787f61aa0..73e50e8d579 100755
--- a/dist/s_docs
+++ b/dist/s_docs
@@ -1,4 +1,10 @@
 #! /bin/sh
 
+# We require doxygen which may not be installed.
+type doxygen > /dev/null 2>&1 || {
+	echo 'doxygen not found, skipping document creation'
+	return 1
+}
+
 # Run doxygen to generate HTML documentation.
 cd ../docs && (cat Doxyfile ; echo "QUIET=YES") | doxygen -