diff --git a/build_docs.sh b/build_docs.sh new file mode 100755 index 0000000000..90bd561e1a --- /dev/null +++ b/build_docs.sh @@ -0,0 +1,18 @@ +#!/bin/bash + + +if which gimli >/dev/null; then + find docs -name "*.md" -exec cat {} > documentation.md \; + gimli -f documentation.md + mv documentation.pdf docs + rm documentation.md +else + echo -e "\nFAILED" + echo "Install Gimli to build the PDF documentation" + echo -e "https://github.com/walle/gimli\n" + exit 1 +fi + + + +