From 1a79e7456c871ca1eecaf5dada85dca0582040b0 Mon Sep 17 00:00:00 2001
From: lethosor <lethosor@gmail.com>
Date: Thu, 11 Aug 2016 18:43:34 -0400
Subject: [PATCH] Add shell script to build docs

Useful for testing docs without changing BUILD_DOCS if it's set to OFF.
---
 docs/build.sh | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100755 docs/build.sh

diff --git a/docs/build.sh b/docs/build.sh
new file mode 100755
index 000000000..d9c0428ad
--- /dev/null
+++ b/docs/build.sh
@@ -0,0 +1,20 @@
+#!/bin/sh
+
+# usage:
+# ./build.sh
+# ./build.sh sphinx-executable
+# JOBS=3 ./build.sh ...
+
+cd $(dirname "$0")
+cd ..
+
+sphinx=sphinx-build
+if [ -n "$1" ]; then
+    sphinx=$1
+fi
+
+if [ -z "$JOBS" ]; then
+    JOBS=2
+fi
+
+"$sphinx" -a -E -q -b html . ./docs/html -w ./docs/_sphinx-warnings.txt -j "$JOBS"